Loading corrupted ".lpo"

[gabrielhdt]

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

1. cd to a new directory
2. Create a file named lambdapi.pkg with the following content

   package_name = bug
   root_path    = a

3. Create a file named f.lp with the following content

   symbol A: TYPE;
   symbol a: A;
   symbol f: A -> A;

4. Create a file named fr.lp with the following content

   require open a.f;
   rule f a --> a;

5. Generate f.lpo with lambdapi check --gen-obj f.lp.
6. Change the package name from a to b, in lambadpi.pkg and fr.lp,

   sed -i 's/a$/b/' lambdapi.pkg
   sed -i 's/a\.f/b.f/' fr.lp

7. Check the file fr.lp.

   lambdapi check fr.lp

   and you should see

   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

[fblanqui]

Are you sure about 423? sign.ml has less lines.

[fblanqui]

The assert false is line 340.

[gabrielhdt]

Ah it must be because I wasn't looking at master, sorry

[fblanqui]

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?

[fblanqui]

f.lp.txt fr.lp.txt lambdapi.pkg.txt

[gabrielhdt]

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?

[fblanqui]

Right, this is perhaps better to do a fatal like in sign.ml, line 272 in read.

[fblanqui]

The error is now Uncaught exception: Not_found on line 2.