The library build fails on Windows 10

mrakgr commented 5 years ago

PS E:\TheoremProving\CubicalAgdaStuff\cubical> make
cabal exec -- fix-agda-whitespace --check
Warning: The exec command is a part of the legacy v1 style of cabal usage.

Please switch to using either the new project style and the new-exec command
or the legacy v1-exec alias as new-style projects will become the default in
the next version of cabal-install. Please file a bug if you cannot replicate a
working v1- use case with the new-style commands.

For more information, see: https://wiki.haskell.org/Cabal/NewBuild

cabal: The program 'fix-agda-whitespace' is required but it could not be
found.

make: *** [GNUmakefile:11: check-whitespace] Error 1

I know that make which I got through Chocolatey works as I needed to use it for Proof General + Coq. I tried cabal install fix-agda-whitespace, but am getting nothing.

Also I get a type error when I try to typecheck the Cubical.Core.Primitives file.

E:\TheoremProving\CubicalAgdaStuff\cubical\Cubical\Core\Primitives.agda:193,3-196,16
A (i ∧ i0) → A (i ∧ i1) !=< A i of type
Set (ℓ-max (ℓ′ (i ∧ i0)) (ℓ′ (i ∧ i1)))
when checking that the inferred type of an application
  A (i ∧ i0) → A (i ∧ i1)
matches the expected type
  A i

This is for ...

-- Heterogeneous filling defined using comp
fill : (A : ∀ i → Type (ℓ′ i))
       {φ : I}
       (u : ∀ i → Partial φ (A i))
       (u0 : A i0 [ φ ↦ u i0 ])
       ---------------------------
       (i : I) → A i
fill A {φ = φ} u u0 i =
  comp (λ j → A (i ∧ j))
       (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
                ; (i = i0) → outS u0 })
       (outS u0)

I do not think this error is related to the build failure which makes it that much more puzzling. I got Agda 2.6.0.1 just now. Should I try going back to 2.6.0?

mrakgr commented 5 years ago

Oh, here is an explanation for the last one. I guess I'll give installing the development version of Agda a shot.

mrakgr commented 5 years ago

PS E:\TheoremProving\CubicalAgdaStuff\agda> cabal v2-install agda agda-mode
Wrote tarball sdist to
E:\TheoremProving\CubicalAgdaStuff\agda\dist-newstyle\sdist\Agda-2.6.1.tar.gz
Wrote tarball sdist to
E:\TheoremProving\CubicalAgdaStuff\agda\dist-newstyle\sdist\fix-agda-whitespace-0.0.4.tar.gz
Resolving dependencies...
Build profile: -w ghc-8.6.5 -O1
In order, the following will be built (use -v for more details):
 - Agda-2.6.1 (lib:Agda, exe:agda, exe:agda-mode) (requires build)
Starting     Agda-2.6.1 (all, legacy fallback)
Building     Agda-2.6.1 (all, legacy fallback)
Warning: Some package(s) failed to build. Try rerunning with -j1 if you can't
see the error.

PS E:\TheoremProving\CubicalAgdaStuff\agda> cabal v2-install agda agda-mode -j1
Wrote tarball sdist to
E:\TheoremProving\CubicalAgdaStuff\agda\dist-newstyle\sdist\Agda-2.6.1.tar.gz
Wrote tarball sdist to
E:\TheoremProving\CubicalAgdaStuff\agda\dist-newstyle\sdist\fix-agda-whitespace-0.0.4.tar.gz
Resolving dependencies...
Build profile: -w ghc-8.6.5 -O1
In order, the following will be built (use -v for more details):
 - Agda-2.6.1 (lib:Agda, exe:agda, exe:agda-mode) (requires build)
[1 of 1] Compiling Main             ( C:\Users\Marko\AppData\Local\Temp\cabal-install.-5016\dist-newstyle\tmp\src-5016\Agda-2.6.1\dist\setup\setup.hs, C:\Users\Marko\AppData\Local\Temp\cabal-install.-5016\dist-newstyle\tmp\src-5016\Agda-2.6.1\dist\setup\Main.o )
Linking C:\Users\Marko\AppData\Local\Temp\cabal-install.-5016\dist-newstyle\tmp\src-5016\Agda-2.6.1\dist\setup\setup.exe ...
Configuring Agda-2.6.1...
Preprocessing executable 'agda-mode' for Agda-2.6.1..
Building executable 'agda-mode' for Agda-2.6.1..
[1 of 2] Compiling Paths_Agda       ( dist\build\agda-mode\autogen\Paths_Agda.hs, dist\build\agda-mode\agda-mode-tmp\Paths_Agda.o )
[2 of 2] Compiling Main             ( src\agda-mode\Main.hs, dist\build\agda-mode\agda-mode-tmp\Main.o )
Linking dist\build\agda-mode\agda-mode.exe ...
Preprocessing library for Agda-2.6.1..
Building library for Agda-2.6.1..
[  1 of 372] Compiling Agda.Interaction.BasicOps[boot] ( src\full\Agda\Interaction\BasicOps.hs-boot, dist\build\Agda\Interaction\BasicOps.o-boot )
[  2 of 372] Compiling Agda.Interaction.Options.IORefs ( src\full\Agda\Interaction\Options\IORefs.hs, dist\build\Agda\Interaction\Options\IORefs.o )
[  3 of 372] Compiling Agda.Syntax.Builtin ( src\full\Agda\Syntax\Builtin.hs, dist\build\Agda\Syntax\Builtin.o )
[  4 of 372] Compiling Agda.Termination.CutOff ( src\full\Agda\Termination\CutOff.hs, dist\build\Agda\Termination\CutOff.o )
[  5 of 372] Compiling Agda.Termination.Semiring ( src\full\Agda\Termination\Semiring.hs, dist\build\Agda\Termination\Semiring.o )
[  6 of 372] Compiling Agda.Utils.AffineHole ( src\full\Agda\Utils\AffineHole.hs, dist\build\Agda\Utils\AffineHole.o )
[  7 of 372] Compiling Agda.Utils.Applicative ( src\full\Agda\Utils\Applicative.hs, dist\build\Agda\Utils\Applicative.o )
[  8 of 372] Compiling Agda.Utils.BiMap ( src\full\Agda\Utils\BiMap.hs, dist\build\Agda\Utils\BiMap.o )
[  9 of 372] Compiling Agda.Utils.Environment ( src\full\Agda\Utils\Environment.hs, dist\build\Agda\Utils\Environment.o )
[ 10 of 372] Compiling Agda.Utils.Except ( src\full\Agda\Utils\Except.hs, dist\build\Agda\Utils\Except.o )
[ 11 of 372] Compiling Agda.Utils.Float ( src\full\Agda\Utils\Float.hs, dist\build\Agda\Utils\Float.o )
[ 12 of 372] Compiling Agda.Utils.Function ( src\full\Agda\Utils\Function.hs, dist\build\Agda\Utils\Function.o )
[ 13 of 372] Compiling Agda.TypeChecking.SizedTypes.Utils ( src\full\Agda\TypeChecking\SizedTypes\Utils.hs, dist\build\Agda\TypeChecking\SizedTypes\Utils.o )
[ 14 of 372] Compiling Agda.Utils.Functor ( src\full\Agda\Utils\Functor.hs, dist\build\Agda\Utils\Functor.o )
[ 15 of 372] Compiling Agda.Utils.Graph.TopSort ( src\full\Agda\Utils\Graph\TopSort.hs, dist\build\Agda\Utils\Graph\TopSort.o )
[ 16 of 372] Compiling Agda.Utils.Haskell.Syntax ( src\full\Agda\Utils\Haskell\Syntax.hs, dist\build\Agda\Utils\Haskell\Syntax.o )
[ 17 of 372] Compiling Agda.Utils.IO    ( src\full\Agda\Utils\IO.hs, dist\build\Agda\Utils\IO.o )
[ 18 of 372] Compiling Agda.Utils.IO.Binary ( src\full\Agda\Utils\IO\Binary.hs, dist\build\Agda\Utils\IO\Binary.o )
[ 19 of 372] Compiling Agda.Utils.IO.Directory ( src\full\Agda\Utils\IO\Directory.hs, dist\build\Agda\Utils\IO\Directory.o )
[ 20 of 372] Compiling Agda.Utils.IO.UTF8 ( src\full\Agda\Utils\IO\UTF8.hs, dist\build\Agda\Utils\IO\UTF8.o )
[ 21 of 372] Compiling Agda.Utils.IO.TempFile ( src\full\Agda\Utils\IO\TempFile.hs, dist\build\Agda\Utils\IO\TempFile.o )
[ 22 of 372] Compiling Agda.Utils.IORef ( src\full\Agda\Utils\IORef.hs, dist\build\Agda\Utils\IORef.o )
[ 23 of 372] Compiling Agda.Utils.Impossible ( src\full\Agda\Utils\Impossible.hs, dist\build\Agda\Utils\Impossible.o )
[ 24 of 372] Compiling Agda.Utils.Empty ( src\full\Agda\Utils\Empty.hs, dist\build\Agda\Utils\Empty.o )
[ 25 of 372] Compiling Agda.Utils.Bag   ( src\full\Agda\Utils\Bag.hs, dist\build\Agda\Utils\Bag.o )
[ 26 of 372] Compiling Agda.ImpossibleTest ( src\full\Agda\ImpossibleTest.hs, dist\build\Agda\ImpossibleTest.o )
[ 27 of 372] Compiling Agda.Auto.NarrowingSearch ( src\full\Agda\Auto\NarrowingSearch.hs, dist\build\Agda\Auto\NarrowingSearch.o )
[ 28 of 372] Compiling Agda.Utils.IntSet.Infinite ( src\full\Agda\Utils\IntSet\Infinite.hs, dist\build\Agda\Utils\IntSet\Infinite.o )
[ 29 of 372] Compiling Agda.Utils.Lens  ( src\full\Agda\Utils\Lens.hs, dist\build\Agda\Utils\Lens.o )
[ 30 of 372] Compiling Agda.Utils.IndexedList ( src\full\Agda\Utils\IndexedList.hs, dist\build\Agda\Utils\IndexedList.o )
[ 31 of 372] Compiling Agda.Interaction.Library.Base ( src\full\Agda\Interaction\Library\Base.hs, dist\build\Agda\Interaction\Library\Base.o )
[ 32 of 372] Compiling Agda.Auto.Options ( src\full\Agda\Auto\Options.hs, dist\build\Agda\Auto\Options.o )
[ 33 of 372] Compiling Agda.Utils.Lens.Examples ( src\full\Agda\Utils\Lens\Examples.hs, dist\build\Agda\Utils\Lens\Examples.o )
[ 34 of 372] Compiling Agda.Utils.Map   ( src\full\Agda\Utils\Map.hs, dist\build\Agda\Utils\Map.o )
[ 35 of 372] Compiling Agda.Utils.Maybe ( src\full\Agda\Utils\Maybe.hs, dist\build\Agda\Utils\Maybe.o )
[ 36 of 372] Compiling Agda.Utils.ListT ( src\full\Agda\Utils\ListT.hs, dist\build\Agda\Utils\ListT.o )
[ 37 of 372] Compiling Agda.Interaction.Options.Warnings ( src\full\Agda\Interaction\Options\Warnings.hs, dist\build\Agda\Interaction\Options\Warnings.o )
[ 38 of 372] Compiling Agda.Interaction.Options.Help ( src\full\Agda\Interaction\Options\Help.hs, dist\build\Agda\Interaction\Options\Help.o )
[ 39 of 372] Compiling Agda.Utils.Memo  ( src\full\Agda\Utils\Memo.hs, dist\build\Agda\Utils\Memo.o )
[ 40 of 372] Compiling Agda.Utils.Monoid ( src\full\Agda\Utils\Monoid.hs, dist\build\Agda\Utils\Monoid.o )
[ 41 of 372] Compiling Agda.Utils.NonemptyList ( src\full\Agda\Utils\NonemptyList.hs, dist\build\Agda\Utils\NonemptyList.o )
[ 42 of 372] Compiling Agda.Utils.Null  ( src\full\Agda\Utils\Null.hs, dist\build\Agda\Utils\Null.o )
[ 43 of 372] Compiling Agda.Utils.Maybe.Strict ( src\full\Agda\Utils\Maybe\Strict.hs, dist\build\Agda\Utils\Maybe\Strict.o )
[ 44 of 372] Compiling Agda.Utils.Parser.ReadP ( src\full\Agda\Utils\Parser\ReadP.hs, dist\build\Agda\Utils\Parser\ReadP.o )
[ 45 of 372] Compiling Agda.Utils.PartialOrd ( src\full\Agda\Utils\PartialOrd.hs, dist\build\Agda\Utils\PartialOrd.o )
[ 46 of 372] Compiling Agda.Utils.POMonoid ( src\full\Agda\Utils\POMonoid.hs, dist\build\Agda\Utils\POMonoid.o )
[ 47 of 372] Compiling Agda.Utils.Pointer ( src\full\Agda\Utils\Pointer.hs, dist\build\Agda\Utils\Pointer.o )
[ 48 of 372] Compiling Agda.Utils.SemiRing ( src\full\Agda\Utils\SemiRing.hs, dist\build\Agda\Utils\SemiRing.o )
[ 49 of 372] Compiling Agda.Utils.Singleton ( src\full\Agda\Utils\Singleton.hs, dist\build\Agda\Utils\Singleton.o )
[ 50 of 372] Compiling Agda.Utils.Cluster ( src\full\Agda\Utils\Cluster.hs, dist\build\Agda\Utils\Cluster.o )
[ 51 of 372] Compiling Agda.Utils.Size  ( src\full\Agda\Utils\Size.hs, dist\build\Agda\Utils\Size.o )
[ 52 of 372] Compiling Agda.Utils.Pretty ( src\full\Agda\Utils\Pretty.hs, dist\build\Agda\Utils\Pretty.o )
[ 53 of 372] Compiling Agda.Utils.Parser.MemoisedCPS ( src\full\Agda\Utils\Parser\MemoisedCPS.hs, dist\build\Agda\Utils\Parser\MemoisedCPS.o )
[ 54 of 372] Compiling Agda.Utils.FileName ( src\full\Agda\Utils\FileName.hs, dist\build\Agda\Utils\FileName.o )

src\full\Agda\Utils\FileName.hs:117:19: error:
    Variable not in scope: and2M :: IO Bool -> IO Bool -> IO Bool
    |
117 |   doesFileExist f `and2M` do
    |                   ^^^^^^^
Warning: Some package(s) failed to build. Try rerunning with -j1 if you can't
see the error.

Oh boy. The -j1 option is cool as I can see the progress of compilation rather wondering whether it froze at some point, but I guess this development branch is too raw.

What should I do now? Maybe I could try some earlier version of the Cubical library. Is there one that is compatible with Agda 2.6.0.1?

I am completely new to this cubical stuff, so I do not need the latest version anyway.

Saizan commented 5 years ago

The v0.1 release is supposed to be compatible with the released version of Agda: https://github.com/agda/cubical/releases/tag/v0.1

agda/master builds most of the time, in my experience, though i never used the v2-install stuff.

About make, you only have fix-agda-whitespace installed if you develop agda, otherwise you can just import the library into your code and start doing things.

mrakgr commented 5 years ago

Thank you for the advice. It would have saved me quite a bit of time had I checked the tags rather than just the branches yesterday. In my experience, time gets wasted when trying out new things unfortunately.

mrakgr commented 5 years ago

Since I have your attention, would you mind answering this SO question? Right now I am going through the paper and copy pasting the code fragments. Is there is a file with all the code there already?

On page 2, there is a slight typo. Unsurprisingly, this suffers from the same drawbacks as it compromises the computational behavior of programs that use these axioms, and even make subsequent proofs more complicated.

and even make should be and even makes.

Thanks for writing the paper by the way, without it I'd have to leave the study of this for later. I've looked for tutorial materials on CCTT, but managed to find nothing apart from this so far. There are papers on CCTT, but they are all expert level. Even when it comes to other proof assistants like RedPRL and RedTT, they barely seem to have any documentation at all. There are lectures on HoTT of course, but as expected it there is a large difference in immersion between seeing somebody writing things on the blackboard and being able to run actual programs.

agda / cubical

The library build fails on Windows 10 #162