[ compat ] with current Idris

[gallais]

Following https://github.com/idris-lang/Idris2/issues/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]

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]

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

[joliss]

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]

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]

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

[gallais]

Have fun!