search

plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.36k stars 307 forks source link

Unrecognized option: --cubical-compatible #991

Closed freeman42x closed 5 months ago

freeman42x commented 5 months ago

When running via precompiled version of Agda 2.6.0.1 for Windows type-checking errors with:

\plfa\src\plfa\part1\Naturals.lagda.md:263,8-51
Unrecognized option: --cubical-compatible
when scope checking the declaration
  import Relation.Binary.PropositionalEquality as Eq

The solution was to install agda via cabal: cabal install Agda-2.6.3

The fact that Agda 2.6.3 is required should be probably clearly documented in the readme.

Hope this helps anyone else running in to the error.

wenkokke commented 5 months ago

Closing, as the fact that Agda 2.6.3 is required is documented in the README.