search

statebox / idris-ct

formally verified category theory library
GNU Affero General Public License v3.0
256 stars 23 forks source link

build times #82

Open Jake-Gillberg opened 4 years ago

Jake-Gillberg commented 4 years ago

Building takes quite a long time and lately has been failing on my measly 2GB ram machine.

Is there a way to have an idris project depend on a pre-compiled target, and a way to publish these targets for the current master branch?

marcosh commented 4 years ago

@andrevidela maybe you're the best one to answer this

Jake-Gillberg commented 4 years ago

For now I just commented out the portions of elba.toml that aren't needed for the pieces that I am working on. This seems like a fine workaround for contribution edits to this library, but not for projects that have idris-ct as a dependency via elba.

andrevidela commented 4 years ago

Sorry I just saw this.

I just bought a computer with 32Gb of ram. … Just kidding, maybe you can have better chances by compling every file separately from the REPL and at the end run idris --install with the IBCs already compiled.

This will also take a long time but at least it won't fail.

Jake-Gillberg commented 4 years ago

Would it make sense to have the build process commit the ibcs to a branch called "compiled" or something?

andrevidela commented 4 years ago

I don't think so, but maybe we could make an official release with the library precompiled