Comments (5)
mrakgr
commented on July 21, 2024
Oh, here is an explanation for the last one. I guess I'll give installing the development version of Agda a shot.
from cubical.
mrakgr
commented on July 21, 2024
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.
from cubical.
Saizan
commented on July 21, 2024
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.
from cubical.
mrakgr
commented on July 21, 2024
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.
from cubical.
mrakgr
commented on July 21, 2024
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.
from cubical.
Related Issues (20)
- Citation.cff HOT 4
- Where should `π₁(RP²)` be? HOT 1
- Duplication of code in the library HOT 3
- Note licence exceptions HOT 2
- Slightly more generalized universes HOT 1
- Remove `isSet` accessors for algebraic structures? HOT 3
- Change the Constructor Name of Sequential Colimits HOT 2
- CI workflow with current agda master HOT 5
- Additions to the powerset module HOT 2
- Some Files are never checked HOT 6
- Suggested heap size for CI HOT 1
- SumMap in Algebra.Ring.BigOps should come from Semirings /Monoids HOT 1
- `make` fails on macOS Sonoma 14.2.1 with Apple Silicon HOT 1
- Algebraic geometry HOT 2
- Figure out why the CommRingSolver doesn't work in this case HOT 5
- Make the CommRingSolver work better with concrete rings
- More elegant construction of ZariskiLattice HOT 2
- Solver for wild categories
- arithmetic operations of Cubical.Data.Rationals is super slow HOT 1
- Naming Convention for Disambiguation HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from cubical.