Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ compat ] with current Idris #2

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Conversation

gallais
Copy link

@gallais gallais commented Apr 12, 2021

Following idris-lang/Idris2#1291 here is an updated version of the code
in this repository to work with the current dev version of idris.

Unfortunately I don't know how to install multiple version in parallel so I can't check
that it works with 0.3.0 too. I suppose I could add CI to this repo if you want to make
sure it does work.

Note that idris2 --build lecture2.ipkg fails because of a missing insertNVarNames.
Adding it to Core.TT would require pulling in new notions like NVar but I'm not
sure whether this is intended (I must admit I don't remember whether lecture 2 had
already covered these topics).

@reswatson
Copy link

Using version 0.3.0

All the ipkgs compile using idris2 --build XXXX.ipkg, except lecture2 as already noted.
Assuming you are in the right directory. And assuming (unlike me at first, being naive at these things) you aren't using a git clone, but are correctly using an unpacked zip file for the code!

I do get these warnings (or similar):

Warning: compiling hole TTImp.Elab.Term.todo_infer_lam
Warning: compiling hole TTImp.Elab.Term.todo_in_part_2
Warning: compiling hole TTImp.Elab.Term.finishIPi
Warning: compiling hole TTImp.Elab.Term.finishILam

@gallais
Copy link
Author

gallais commented May 7, 2021

Yep the files have holes for the exercises you're supposed to solve yourself :D

@joliss
Copy link

joliss commented Jun 7, 2021

Oh my gosh, thanks so much for the work you put into getting this running with Idris 2!

I tried applying this and compiling TinyIdris-v1, but I'm still running into a compile error:

SPLV20 $ hub merge --ff https://github.com/edwinb/SPLV20/pull/2
From https://github.com/edwinb/SPLV20
 * branch            refs/pull/2/head -> FETCH_HEAD
Updating b401de0..28eb811
Fast-forward (no commit created; -m option ignored)
 Code/Lecture1/Core/Core.idr                             | 17 +++++++++++++----
 Code/Lecture1/lecture1.ipkg                             | 11 +++++++++++
...
 38 files changed, 325 insertions(+), 129 deletions(-)

SPLV20 $ idris2 --version
Idris 2, version 0.3.0

SPLV20 $ cd TinyIdris-v1

SPLV20/TinyIdris-v1 $ idris2 --build tinyidris.ipkg
1/39: Building Data.Bool.Extra (src/Data/Bool/Extra.idr)
2/39: Building Text.Lexer.Core (src/Text/Lexer/Core.idr)
3/39: Building Text.Quantity (src/Text/Quantity.idr)
4/39: Building Text.Token (src/Text/Token.idr)
5/39: Building Text.Lexer (src/Text/Lexer.idr)
6/39: Building Parser.Lexer.Common (src/Parser/Lexer/Common.idr)
7/39: Building Text.Parser.Core (src/Text/Parser/Core.idr)
8/39: Building Text.Parser (src/Text/Parser.idr)
9/39: Building Utils.String (src/Utils/String.idr)
10/39: Building Parser.Lexer.Package (src/Parser/Lexer/Package.idr)
11/39: Building Parser.Rule.Common (src/Parser/Rule/Common.idr)
12/39: Building Parser.Rule.Package (src/Parser/Rule/Package.idr)
13/39: Building Core.TT (src/Core/TT.idr)
14/39: Building Text.Literate (src/Text/Literate.idr)
Error: While processing right hand side of reduce. While processing right hand side of reduce,blank_content. Sorry, I can't find any elaboration which works.
All errors:
If Prelude.List.length: When unifying List String and List1 ?a.
Mismatch between: List String and List1 ?a.

src/Text/Literate.idr:72:61--72:68
    |
 72 |     blank_content = fastAppend (replicate (length (forget $ lines x)) "\n")
    |                                                             ^^^^^^^

If Prelude.Strings.length: When unifying List String and List1 ?a.
Mismatch between: List String and List1 ?a.

src/Text/Literate.idr:72:61--72:68
    |
 72 |     blank_content = fastAppend (replicate (length (forget $ lines x)) "\n")
    |                                                             ^^^^^^^

Am I doing something wrong?

@gallais
Copy link
Author

gallais commented Jun 7, 2021

Am I doing something wrong?

I don't think so. As I said in the original message: I ported the code using
the development version of Idris2 I had at the time. I guess that in the 0.3.0
version lines has not yet been given the String -> List1 String type and
instead has type String -> List String.

You should be able to make the error go away by removing the calls to forget.

@joliss
Copy link

joliss commented Jun 7, 2021

Ah, thank you, I'd missed that for some reason. It compiles fine with Idris2 built from the master branch!

@gallais
Copy link
Author

gallais commented Jun 7, 2021

Have fun!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants