agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
454 stars 139 forks source link

`Unknown warning flag: UnsupportedIndexedMatch` #982

Closed vezwork closed 1 year ago

vezwork commented 1 year ago

I just cloned this repo, added it to my .agda/libraries, and added it as a dependency in my project's agda-lib.

In a file file.agda I have

{-# OPTIONS --cubical #-}

module file where

open import Cubical.HITs.FiniteMultiset.Base public

and when I load with Agda, I get this error:

Unknown warning flag: UnsupportedIndexedMatch. See --help=warning.
when scope checking the declaration
  open import Cubical.HITs.FiniteMultiset.Base public

I looked through this repo and found that I can use

{-# OPTIONS --cubical -WnoUnsupportedIndexedMatch #-}

but then when I load I get another error, now:

Unknown warning flag: UnsupportedIndexedMatch. See --help=warning.

I'm on MacOS Ventura with an M1 chip, using VSCode, with Agda version 2.6.2.2 installed. I can give more details on my libraries or agda-lib if that is helpful.

vezwork commented 1 year ago

I think this may be because I need Agda version 2.6.3 or above. I am attempting to install it. Agda 2.6.2 is the latest version on brew for OSX.

vezwork commented 1 year ago

I installed Agda using Cabal, which has version 2.6.3 currently. I updated my agda-mode extension to use my Cabal installed Agda. Now everything is working! :)

vezwork commented 1 year ago

It is confusing because it seems that the latest version of Agda is 2.6.4 but it has not yet made its way to Brew or Cabal.

felixwellen commented 1 year ago

Agda 2.6.4 is the current development version of Agda. The latest release is 2.6.3 (which might still be in the process of being released). For anyone with a problem to get Agda 2.6.3: Just checkout the tag v0.4 of this library with

git checkout v0.4

Then you can use Agda 2.6.2.2. For older versions of Agda, look at the README.md to figure out which tag you can use.