Cubical not typechecking upon install

[cosmoviola]

I am trying to install the Cubical library for agda. I already had an existing agda installation, but I followed the directions here and set Cabal to overwrite the existing installation using the --overwrite-policy=always flag. This seemed to work, but when I run make to typecheck the cubical files, as suggested in the installation instructions, I get the following error: cubical_build_error.txt. The last file to fail to typecheck is Cubical/Data/FinData/Properties.agda with unsolved metavariables.

Did I make a mistake when installing the library? I would appreciate suggestions as to how to fix this.

[cosmoviola]

Adding @tlringer because we are working together on a project.

[felixwellen]

I looks like you are using a version of agda newer than 2.6.2.2 (this is the version we use to check the library) - can you check that with agda --version?

[plt-amy]

This is a known regression on Agda's master branch relative to 2.6.2.2 (https://github.com/agda/agda/issues/6047 edit got the last two digits backwards originally, nice reminder of my dyslexia). The cubical library does not track Agda's master branch.

[tlringer]

Oh, thank you! Is this documented anywhere? The installation instructions we followed didn't mention that the cubical library tracks on a different version of Agda. (We indeed were working with 2.6.3, but the instructions we followed for installing cubical actually landed us on 2.6.3 by default.)

[tlringer]

In particular, I'd like to suggest in the meantime that if this tracks on specific versions of Agda, the specific supported versions are documented here for new users, or otherwise the instructions provided default to that specific installation (latter is probably better since then you don't need to modify the INSTALL.md every time).

[felixwellen]

Here is a draft, comments welcome:

https://github.com/agda/cubical/blob/install_latest_release/INSTALL.md

I added how to checkout the tag for the latest release, for cabal-v2, cabal sandbox and stack-instructions. I only use stack myself, but I cannot imagine how that step could be different with other build tools. I also made the "latest release of agda" in the beginning of the page more visible by turning it into a link to a page that tells you which agda version is the latest release.

[felixwellen]

Now it is also a draft PR: https://github.com/agda/cubical/pull/933

[mortberg]

Not about the topic of this PR, but @cosmoviola and @tlringer are very welcome to join our Univalent Agda Discord server: https://discord.gg/yjTKHzepMx

There is a channel for this library there and you're very welcome to join and ask any questions you might have about the library or installation issues!

[felixwellen]

I am happy with PR #933 now - @cosmoviola , @tlringer please have a look and let me know if you think the problem is resolved. Thanks for reporting! Everyone with rights to do so: feel free to improve the PR without asking - I put the branch on this repo, so you can just push to it.

[tlringer]

LGTM. @cosmoviola , did you manage to get this working with the updated instructions?

[cosmoviola]

I just ran it, the updated instructions fix the problem. Looks good to me.

[felixwellen]

Ok, good - I'll merge that then.

[felixwellen]

Done, closing issue since it is resolved.