Unexpected type checking behavior

[nicolabotta]

The program

> module NonNegRational.tests.Main

> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties
> import Fraction.Fraction
> import PNat.PNat
> import Nat.Positive

> %default total
> %auto_implicits off

> postulate sumOneLemma : {m, n, d : Nat} -> m + n = S d -> 
>                         fromFraction (m, Element (S d) MkPositive) 
>                         + 
>                         fromFraction (n, Element (S d) MkPositive) 
>                         = 
>                         1

> x  : NonNegRational
> x  = fromFraction (9, Element 10 MkPositive) 

> y  : NonNegRational
> y  = fromFraction (1, Element 10 MkPositive) 

> p : x + y = 1
> -- p = sumOneLemma Refl

type checks fine. But if one uncomments the last line, the type checker bails out after about 15 minutes:

Type checking ./NonNegRational/tests/Test1.lidr
Killed

You should be able to reproduce this behavior by downloading https://gitlab.pik-potsdam.de/botta/IdrisLibs and doing

make libs; time idris NonNegRational/tests/Test1.lidr

Any idea how to avoid this problem?

[ahmadsalim]

@nicolabotta For me it failed to compile on the latest Idris version (specifically, I had problems with Nat.Positive). Do you have an idea how to fix this? If it is not to too hard, could you kindly try to inline the necessary definitions so it can be checked in a self-contained way? Thanks!

[nicolabotta]

@ahmadsalim This is strange. The output of

make libs; time idris NonNegRational/tests/Test1.lidr

on a fresh installation of IdrisLibs and with Idris-dev-ff776da on my system is

nicola@cirrus:~/lala/IdrisLibs-master-6c995a0099acf81355549b7272e5313476043778$ make libs; time idris NonNegRational/tests/Test1.lidr
find . \
  -not \( -path "./examples" -prune \) \
  -not \( -path "./papers" -prune \) \
  -not \( -path "./tmp" -prune \) \
  -not \( -path "./GenericSimpleProb" -prune \) \
  -not \( -path "./SequentialDecisionProblems" -prune \) \
  -not \( -path "./*/tests" -prune \) \
  -not \( -path "./*/open_issues" -prune \) \
  -name '*.lidr' | xargs -n 1 idris +RTS -K32000000 -RTS -p contrib -p effects -V --check
Type checking ./Unique/Predicates.lidr
Type checking ././Equality/Properties.lidr
Type checking ./Sigma/Sigma.lidr
Type checking ././BoundedNat/BoundedNat.lidr
Type checking ./Finite/Predicates.lidr
Type checking ./Basic/Operations.lidr
Type checking ./Fin/Operations.lidr
Type checking ./Pair/Properties.lidr
Type checking ./Fun/Operations.lidr
Type checking ./Fun/Properties.lidr
Type checking ./Fin/Properties.lidr
Type checking ./Basic/Properties.lidr
Type checking ./Isomorphism/Operations.lidr
Type checking ./Isomorphism/Properties.lidr
Type checking ./Nat/LTEProperties.lidr
Type checking ./Nat/BasicProperties.lidr
Type checking ./Nat/LTProperties.lidr
Type checking ./Rel/Preorder.lidr
Type checking ./Rel/TotalPreorder.lidr
Type checking ./Rel/TotalPreorderOperations.lidr
Type checking ./Decidable/Predicates.lidr
Type checking ./Pairs/Operations.lidr
Type checking ./Exists/Operations.lidr
Type checking ./Vect/Operations.lidr
Type checking ./Finite/Operations.lidr
Type checking ./Sigma/Operations.lidr
Type checking ./Vect/Properties.lidr
Type checking ./Finite/Properties.lidr
Type checking ./Sigma/Properties.lidr
Type checking ./BoundedNat/Operations.lidr
Type checking ././BoundedNat/Properties.lidr
Type checking ./Nat/Predicates.lidr
Type checking ./Nat/Operations.lidr
Type checking ./Nat/OperationsProperties.lidr
Type checking ./Nat/Divisor.lidr
Type checking ./Nat/DivisorOperations.lidr
Type checking ./Nat/DivisorProperties.lidr
Type checking ./Nat/GCD.lidr
Type checking ./Nat/GCDEuclid.lidr
Type checking ./Nat/GCDOperations.lidr
Type checking ./Nat/GCDProperties.lidr
Type checking ././Nat/GCDAlgorithm.lidr
Type checking ././Nat/Coprime.lidr
Type checking ./Subset/Operations.lidr
Type checking ./Subset/Properties.lidr
Type checking ././Nat/Positive.lidr
Type checking ././Nat/CoprimeProperties.lidr
Type checking ././Decidable/Properties.lidr
Type checking ././PNat/PNat.lidr
Type checking ./PNat/Operations.lidr
Type checking ././PNat/Properties.lidr
Type checking ././Num/Refinements.lidr
Type checking ./Matrix/Matrix.lidr
Type checking ./Num/Operations.lidr
Type checking ./Matrix/Operations.lidr
Type checking ././Num/Properties.lidr
Type checking ./Unit/Properties.lidr
Type checking ./Void/Properties.lidr
Type checking ./List/Operations.lidr
Type checking ././List/Properties.lidr
Type checking ././Unique/Properties.lidr
Type checking ./Fraction/Fraction.lidr
Type checking ./Fraction/BasicOperations.lidr
Type checking ./Fraction/Normal.lidr
Type checking ./Fraction/BasicProperties.lidr
Type checking ./Fraction/Predicates.lidr
Type checking ./Fraction/EqProperties.lidr
Type checking ./Fraction/LTEProperties.lidr
Type checking ./Fraction/Normalize.lidr
Type checking ./Fraction/NormalizeProperties.lidr
Type checking ./NonNegRational/NonNegRational.lidr
Type checking ./NonNegRational/BasicOperations.lidr
Type checking ./NonNegRational/BasicProperties.lidr
Type checking ./NonNegRational/Predicates.lidr
Type checking ./NonNegRational/LTEProperties.lidr
Type checking ./NonNegRational/Measures.lidr
Type checking ./NonNegRational/MeasureProperties.lidr
Type checking ./SimpleProb/SimpleProb.lidr
Type checking ./SimpleProb/BasicOperations.lidr
Type checking ./SimpleProb/BasicProperties.lidr
Type checking ./SimpleProb/MonadicOperations.lidr
Type checking ././SimpleProb/MonadicProperties.lidr
Type checking ././SimpleProb/Measures.lidr
Type checking ././LocalEffect/Exception.lidr
Type checking ././LocalEffect/StdIO.lidr
Type checking ./Identity/Operations.lidr
Type checking ././Identity/Properties.lidr
Type checking ././Opt/Operations.lidr
Type checking ././Fun/Predicates.lidr
Type checking ./NonNegRational/tests/Test1.lidr
*NonNegRational/tests/Test1> 

In particular, Nat/Positive type checks fine. It is of course possible that the current Idris version has broken some components of IdrisLibs. I cannot install the current Idris version on my system because of #3350.

Implementing a self-contained example is not going to be doable in a reasonable time, I am afraid. If you try to type check Test1.lidr directly (which should not work because of #3326):

nicola@cirrus:~/lala/IdrisLibs-master-6c995a0099acf81355549b7272e5313476043778$ make clean
find . -name '*.ibc' -delete
find . -name '*~' -delete
nicola@cirrus:~/lala/IdrisLibs-master-6c995a0099acf81355549b7272e5313476043778$ idris NonNegRational/tests/Test1.lidr

you will see that Test1.lidr has too many dependencies for deriving a self-contained example. Thanks for looking into this issue! Best, Nicola

[nicolabotta]

@ahmadsalim What was the specific problem with Nat.Positive? Nat.Positive is a very small component and it should be easy to fix the problem.

[ahmadsalim]

@nicolabotta

I get the following error during compilation:

...
Type checking ./PNat/Properties.lidr
Type checking ./Fraction/Normal.lidr
Type checking ././Fraction/BasicProperties.lidr
Type checking ./Fraction/Predicates.lidr
./Fraction/Predicates.lidr:16:7:No such variable Nat.Positive.Positive
./Fraction/Predicates.lidr:21:6:No such variable Nat.Positive.Positive
...

[nicolabotta]

Is this what you would expect? The name Positive does not apper in ./Fraction/Predicates.lidr at all. Thus, the error seems, to say the least, questionable. Also notice that with Idris-dev-ff776da

idris +RTS -K32000000 -RTS -p contrib -V Fraction/Predicates.lidr

yields no errors:

nicola@cirrus:~/lala/IdrisLibs-master-6c995a0099acf81355549b7272e5313476043778$ idris +RTS -K32000000 -RTS -p contrib -V Fraction/Predicates.lidr
Type checking ./Sigma/Sigma.lidr
Type checking ./Pairs/Operations.lidr
Type checking ./Basic/Operations.lidr
Type checking ./Nat/LTEProperties.lidr
Type checking ./Nat/BasicProperties.lidr
Type checking ./Nat/LTProperties.lidr
Type checking ./Nat/Predicates.lidr
Type checking ./Nat/Operations.lidr
Type checking ./Nat/OperationsProperties.lidr
Type checking ./Basic/Properties.lidr
Type checking ./Pair/Properties.lidr
Type checking ./Fun/Operations.lidr
Type checking ./Fun/Properties.lidr
Type checking ./Isomorphism/Operations.lidr
Type checking ./Isomorphism/Properties.lidr
Type checking ./Fin/Operations.lidr
Type checking ./Fin/Properties.lidr
Type checking ./Rel/Preorder.lidr
Type checking ./Rel/TotalPreorder.lidr
Type checking ./Rel/TotalPreorderOperations.lidr
Type checking ./Decidable/Predicates.lidr
Type checking ./Exists/Operations.lidr
Type checking ./Vect/Operations.lidr
Type checking ./Finite/Predicates.lidr
Type checking ./Finite/Operations.lidr
Type checking ./Sigma/Operations.lidr
Type checking ./Vect/Properties.lidr
Type checking ./Finite/Properties.lidr
Type checking ./Subset/Operations.lidr
Type checking ./Unique/Predicates.lidr
Type checking ./Subset/Properties.lidr
Type checking ./Nat/Positive.lidr
Type checking ./PNat/PNat.lidr
Type checking ./PNat/Operations.lidr
Type checking ./Fraction/Fraction.lidr
Type checking ./Fraction/Predicates.lidr
*Fraction/Predicates> :q
Bye bye
nicola@cirrus:~/lala/IdrisLibs-master-6c995a0099acf81355549b7272e5313476043778$

Perhaps a bug introduced between ff776da and the current Idris version?

[nicolabotta]

@ahmadsalim I could now install 0.99 (please, see #3350) and confirm your results. I think this is an Idris bug, but I have added import Nat.Positive to Fraction/Predicates and to Fraction/LTEProperties. Now make libs yields no errors with 0.99-git:5245054.

[ahmadsalim]

@nicolabotta Great, thanks for confirming the issue. I had trouble installing 0.99 so I could not test it before.

PS: Is there any reason why you do not use .ipkg instead of a Makefile?

[nicolabotta]

@ahmadsalim "Is there any reason why you do not use .ipkg instead of a Makefile?" : no, no particular reason. What are the advantages of .ipkg files against make files?

[ahmadsalim]

They automate certain task like building (making sure to find the optimal order), installation (making sure everything is in the right place), removing and REPL, provide more meta-information and allow you to set flags. Please, see http://docs.idris-lang.org/en/latest/tutorial/packages.html?highlight=package .

[nicolabotta]

@ahmadsalim I do not know how to write a .ipkg file and automate finding the optimal order for IdrisLibs. I might be missing something, of course. If you have a concrete suggestion on how to improve the current Makefile by means of a .ipkg file, I would be happy to add it as an alternative build method to the current Makefile.

[ahmadsalim]

@nicolabotta It would be something like:

package sequential-decision-problems

sourceloc = git://gitlab.pik-potsdam.de/botta/IdrisLibs.git
bugtracker = https://gitlab.pik-potsdam.de/botta/IdrisLibs/issues

opts = ‹options›
pkgs = ‹packages›
modules = ‹modules›

[nicolabotta]

@ahmadsalim Thanks, Ahmad, I'll give it a try. The main problem with .ipkg files is computing <modules>. If I knew a way of computing an optimal order for building the .ibc files of the library, I could put the result of such computation here, see the discussion on the advantages and limitations of .ipkg files in #3324. But I do not know how to make such computation. One would ideally start with those components that have the least number of import directive. I can of course fill in <modules> manually. But, for large collections of components, this is going to be a pain. Best, Nicola

[ahmadsalim]

@nicolabotta You should just list the modules in the order you prefer, as far as I understand you do not have to perform any computation manually.

You could also consider splitting up your different libraries in separate ipkgs if you find that there are too many things in one package.

[jfdm]

@nicolabotta Given a list of modules specified in an ipkg file, Idris will compute for itself a build order from that list. You do not have to compute a 'special' ordering of modules in the ipkg field, any ordering will do. We discussed this in #3324. While you do have to list the modules manually in the first place it, it is something you nonetheless still have to do.

I understand that for a large extant project it will be cumbersome, but worth the effort. In fact a simple bash script can be used to obtain a list of the modules in alphabetical order:

 grep -E -e "^module " `find . -iname "*.idr"` | awk -F"module" '{print $2}' | sort -n

This must be executed in the top level directory of the intended package.

[nicolabotta]

@ahmadsalim @jfdm I know that I can list the modules in the order that I prefer, but then I do not see obvious advantages in using Idris packages instead of make. In fact, with Idris packages, I have to manually maintain a list of files to be type check which I can avoid using make. If I go the manual way, I would like to have at least the advantage of being able to first build those files that have less dependencies, for instance, to be able to avoid #3326.

I have committed a tentative IdrisLibs.ipkg file to the repository. idris --build IdrisLibs.ipkg fails at building LocalEffect.Exception. Manual building LocalEffect.Exception and make libswork fine. Is it possible that there is a problem with

opts = "+RTS -K32000000 -RTS -p contrib -p effects" 

and that the -p effects option is ignored?

[ahmadsalim]

@nicolabotta You should have contrib and effects under pkgs. If you prefer, you could instead have the Makefile task generate the ipkg file once in a while which will provide the advantage of both things.

[nicolabotta]

@ahmadsalim Thanks, that works fine

@jfdm I have problems understanding the logic of .ipkg files. I have an IdrisLibs.ipkg example in IdrisLibs that works fine. I have now added a Basic.ipkg file to the IdrisLibs/Basic directory. This directory contains three files:

Basic.ipkg
Operations.lidr
Properties.lidr

The Basic.ipkgfile reads

package Basic

sourceloc = git://gitlab.pik-potsdam.de/botta/IdrisLibs.git
bugtracker = https://gitlab.pik-potsdam.de/botta/IdrisLibs/issues

opts = "-i .. --sourcepath .. +RTS -K32000000 -RTS"

-- pkgs = 

modules = Basic.Operations
        , Basic.Properties

The -i .. --sourcepath .. options work as one would expect: both

idris -i .. --sourcepath .. +RTS -K32000000 -RTS --check Operations.lidr 

and

idris -i .. --sourcepath .. +RTS -K32000000 -RTS --check Properties.lidr 

terminate without errors. Still, under these premises. idris --build Basic.ipkg fails

Can't find import Basic/Operations

What am I doing wrong here?