Parse error in cubical-0.3 Primitives

[DavidJaz]

I'm trying to play the "HoTT Game", and this uses cubical-0.3. When trying to load the first file, however, I get a parse error:

.../cubical-0.3/Cubical/Core/Primitives.agda:37,14: Parse error Set<ERROR> to Type ; Setω ...

which occurs during the renaming of "Set" to "Type". I'm using Agda version 2.6.2-b7da577. I'm confused at what to do here.

Here's some context for those lines:

open import Agda.Primitive public
  using    ( Level )
  renaming ( lzero to ℓ-zero
           ; lsuc  to ℓ-suc
           ; _⊔_   to ℓ-max
           ; Set    to Type
           ; Setω  to Typeω )
open import Agda.Builtin.Sigma public

I've also opened an issue on cubical itself.

[Jlh18]

Hi there, it would be great if we could call on discord or something as I would be a bit rubbish just trying to help you here. If that's not ok then I'll try my best

[DavidJaz]

Sure, thank you. How do I find you?

[Jlh18]

we could try jitsi - https://meet.jit.si/HumanFacultiesIncreaseSeemingly

[Jlh18]

if youre free now that is

[DavidJaz]

I reinstalled Agda and it worked. Thanks!

[Jlh18]

Great. I hope you enjoy the game :)

[antoinelab01]

Hi! I also got exactly the same issue while trying to play the HoTT game. I tried uninstalling and reinstalling Agda but it didn't work.

[Jlh18]

Since the last time this issue was brought up I added detailed instructions on installing using Nix, which I think is worth trying instead. How did you try to install it?

[antoinelab01]

Thanks for the answer. I install agda via sudo apt install agda-bin and sudo apt install agda-mode. I'll try another method to see if that works.

[antoinelab01]

I tried the Nix installation but I get the following error message when trying to load 1FundamentalGroup/Quest0.agda. Any idea what could cause this?

Failed to find source of module Cubical.Syntax.⟨⟩ in any of the
following locations:
  /nix/store/wsk8knpjchxj805faidblcd16vzphcw2-cubical-0.4prec3e097a/Cubical/Syntax/⟨⟩.agda
  /nix/store/wsk8knpjchxj805faidblcd16vzphcw2-cubical-0.4prec3e097a/Cubical/Syntax/⟨⟩.lagda
  /home/antoine/Documents/agda/TheHoTTGame/Cubical/Syntax/⟨⟩.agda
  /home/antoine/Documents/agda/TheHoTTGame/Cubical/Syntax/⟨⟩.lagda
  /nix/store/mxd6b9c8fgnv3qq34jly0bsq513b111v-Agda-2.6.2.1-data/share/ghc-8.10.7/x86_64-linux-ghc-8.10.7/Agda-2.6.2.1/lib/prim/Cubical/Syntax/⟨⟩.agda
  /nix/store/mxd6b9c8fgnv3qq34jly0bsq513b111v-Agda-2.6.2.1-data/share/ghc-8.10.7/x86_64-linux-ghc-8.10.7/Agda-2.6.2.1/lib/prim/Cubical/Syntax/⟨⟩.lagda
when scope checking the declaration
  open import Cubical.Syntax.⟨⟩

[Jlh18]

are you working inside the nix environment? You should launch emacs from a nix terminal in order to get things working

[antoinelab01]

Yes, I launched doom from nix-shell.

[Jlh18]

I tried the Nix installation but I get the following error message when trying to load 1FundamentalGroup/Quest0.agda. Any idea what could cause this?

Failed to find source of module Cubical.Syntax.⟨⟩ in any of the
following locations:
  /nix/store/wsk8knpjchxj805faidblcd16vzphcw2-cubical-0.4prec3e097a/Cubical/Syntax/⟨⟩.agda
  /nix/store/wsk8knpjchxj805faidblcd16vzphcw2-cubical-0.4prec3e097a/Cubical/Syntax/⟨⟩.lagda
  /home/antoine/Documents/agda/TheHoTTGame/Cubical/Syntax/⟨⟩.agda
  /home/antoine/Documents/agda/TheHoTTGame/Cubical/Syntax/⟨⟩.lagda
  /nix/store/mxd6b9c8fgnv3qq34jly0bsq513b111v-Agda-2.6.2.1-data/share/ghc-8.10.7/x86_64-linux-ghc-8.10.7/Agda-2.6.2.1/lib/prim/Cubical/Syntax/⟨⟩.agda
  /nix/store/mxd6b9c8fgnv3qq34jly0bsq513b111v-Agda-2.6.2.1-data/share/ghc-8.10.7/x86_64-linux-ghc-8.10.7/Agda-2.6.2.1/lib/prim/Cubical/Syntax/⟨⟩.lagda
when scope checking the declaration
  open import Cubical.Syntax.⟨⟩

I just tried my own setup for Nix and realized this is a general problem. I will raise it with the person who made the Nix stuff