search

statebox / idris-ct

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

Can't build using elba 0.3.2 #61

Closed AyeGill closed 5 years ago

AyeGill commented 5 years ago

When building using elba 0.3.2, idris 1.3.2, compilation always fails on MonoidalCategory.MonoidalCategory - it stops there for a long time, then fails with essentially no error message. Trying to compile the file manually with Idris works fine.

$ elba --version
elba 0.3.2
$ idris --version
1.3.2
$ elba build
       [1/2] Resolving dependencies...
       [2/2] Building targets...
    Building statebox/idris-ct 0.1.0 (dir+/home/eigil/projects/idris-ct) [3605e7ee..]
   Compiling Basic.Category [statebox/idris-ct]
   Compiling Basic.ConstantFunctor [statebox/idris-ct]
   Compiling Basic.Functor [statebox/idris-ct]
   Compiling Basic.Isomorphism [statebox/idris-ct]
   Compiling Basic.NaturalIsomorphism [statebox/idris-ct]
   Compiling Basic.NaturalTransformation [statebox/idris-ct]
   Compiling Cats.CatsAsCategory [statebox/idris-ct]
   Compiling Cats.FunctorsAsCategory [statebox/idris-ct]
   Compiling CoLimits.CoCone [statebox/idris-ct]
   Compiling CoLimits.CoConeCat [statebox/idris-ct]
   Compiling CoLimits.CoLimit [statebox/idris-ct]
   Compiling CoLimits.CoLimitAsInitialObject [statebox/idris-ct]
   Compiling CoLimits.CoProduct [statebox/idris-ct]
   Compiling CoLimits.InitialObject [statebox/idris-ct]
   Compiling CoLimits.InitialObjectAsCoLimit [statebox/idris-ct]
   Compiling CoLimits.Pushout [statebox/idris-ct]
   Compiling CommutativeDiagram.Diagram [statebox/idris-ct]
   Compiling Discrete.DiscreteCategory [statebox/idris-ct]
   Compiling Discrete.FunctionAsFunctor [statebox/idris-ct]
   Compiling Dual.DualCategory [statebox/idris-ct]
   Compiling Dual.DualFunctor [statebox/idris-ct]
   Compiling Empty.EmptyCategory [statebox/idris-ct]
   Compiling Empty.EmptyFunctor [statebox/idris-ct]
   Compiling Free.FreeFunctor [statebox/idris-ct]
   Compiling Free.Graph [statebox/idris-ct]
   Compiling Free.Path [statebox/idris-ct]
   Compiling Free.PathCategory [statebox/idris-ct]
   Compiling Idris.EitherAsCoProduct [statebox/idris-ct]
   Compiling Idris.FunctorAsCFunctor [statebox/idris-ct]
   Compiling Idris.TypesAsCategory [statebox/idris-ct]
   Compiling Idris.TypesAsCategoryExtensional [statebox/idris-ct]
   Compiling Lens.Lens [statebox/idris-ct]
   Compiling Lens.SimpleLens [statebox/idris-ct]
   Compiling Limits.Limit [statebox/idris-ct]
   Compiling Limits.Pullback [statebox/idris-ct]
   Compiling Limits.TerminalObject [statebox/idris-ct]
   Compiling Monad.IOMonad [statebox/idris-ct]
   Compiling Monad.KleisliCategory [statebox/idris-ct]
   Compiling Monad.Monad [statebox/idris-ct]
   Compiling Monad.VerifiedMonadAsMonad [statebox/idris-ct]
   Compiling Monoid.Monoid [statebox/idris-ct]
   Compiling Monoid.MonoidAsCategory [statebox/idris-ct]
   Compiling Monoid.MonoidMorphism [statebox/idris-ct]
   Compiling Monoid.MonoidMorphismAsFunctor [statebox/idris-ct]
   Compiling Monoid.MonoidsCategory [statebox/idris-ct]
   Compiling MonoidalCategory.MonoidalCategory [statebox/idris-ct]
     [error] Couldn't build library target for statebox/idris-ct 0.1.0 (dir+/home/eigil/projects/idris-ct)
> "idris" "--check" "-p" "contrib" "MonoidalCategory/MonoidalCategory.lidr"

error: one or more packages couldn't be built
marcosh commented 5 years ago

@AyeGill thanks for submitting the issue.

I think the error is due to this Elba bug. With the 0.3.2 version they reduced (but not removed) its incidence. The long compilation time of the Monad/KleisliCategory module is problematic for the concurrency of Elba and it crashes.

If you want to build with Elba, just remove Monad/KleisliCategory from the modules list.

Otherwise, you can build it directly with Idris

AyeGill commented 5 years ago

Thanks for the quick response :)