lambdapi
lambdapi copied to clipboard
Loading corrupted ".lpo"
Symptoms
Lambdapi raises assert false
when the package_path
of the related lambdapi.pkg
changes and that another file from the same package is imported (from a lpo
).
How to reproduce
-
cd
to a new directory - Create a file named
lambdapi.pkg
with the following contentpackage_name = bug root_path = a
- Create a file named
f.lp
with the following contentsymbol A: TYPE; symbol a: A; symbol f: A -> A;
- Create a file named
fr.lp
with the following contentrequire open a.f; rule f a --> a;
- Generate
f.lpo
withlambdapi check --gen-obj f.lp
. - Change the package name from
a
tob
, inlambadpi.pkg
andfr.lp
,sed -i 's/a$/b/' lambdapi.pkg sed -i 's/a\.f/b.f/' fr.lp
- Check the file
fr.lp
.
and you should seelambdapi check fr.lp
Uncaught exception: File "src/core/sign.ml", line 340, characters 24-30: Assertion failed.
Possible solution
Just mention that the generated objects are out of date?
Edit: corrected error message
Are you sure about 423? sign.ml has less lines.
The assert false is line 340.
Ah it must be because I wasn't looking at master, sorry
Right, we could add some error message before assert false saying that some lpo file is maybe out of date, but we should keep the assert false, don't you think so?
Right, we could add some error message before assert false saying that some lpo file is maybe out of date, but we should keep the assert false, don't you think so?
Rather than using a fatal
?
Right, this is perhaps better to do a fatal like in sign.ml, line 272 in read.
The error is now Uncaught exception: Not_found
on line 2.