search

statebox / idris-ct

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

Add idris2 files #55

Closed andrevidela closed 5 years ago

andrevidela commented 5 years ago

I took the Idris2 branch and files and put it into a subfolder. This will allow us to keep track which files have been ported and which ones have not.

clayrat commented 5 years ago

This currently won't work for Idris2 because there's no sourcedir option; but see https://github.com/edwinb/Idris2/pull/136/

andrevidela commented 5 years ago

It does work for me when I run idris2 --build idris-ct.ipkg in the directory idris2 (as I've written in the Readme)

I think that's good enough for this PR, specially since we don't want to merge the two code bases quite yet.

andrevidela commented 5 years ago

I felt fancy so I wrote a tiny script that compares the file tree between src and idris2 and returns the files which were not converted. Here is the current output:

missing:
/PointedTypes/PointedTypesAsCategory
/CoLimits/Pushout
/CoLimits/InitialObjectAsCoLimit
/CoLimits/CoLimitAsInitialObject
/CoLimits/CoCone
/CoLimits/CoLimit
/CoLimits/CoConeCat
/Monad/VerifiedMonadAsMonad
/Monad/KleisliCategory
/Monad/Monad
/Monad/IOMonad
/Lens/SimpleLens
/Lens/Lens
/CommutativeDiagram/Diagram
/Limits/Pullback
/Limits/TerminalObject
/Limits/Limit
/Basic/ConstantFunctor
/Empty/EmptyCategory
/Empty/EmptyFunctor
/Cats/FunctorsAsCategory
/CategoryReasoning

completion rate: 0.6271186440677966
marcosh commented 5 years ago

this is nice! Locally on my machine the completion rate is 0.53. Now I'll try to port some of the span stuff I'm working on