lambdapi icon indicating copy to clipboard operation
lambdapi copied to clipboard

Loading corrupted ".lpo"

Open gabrielhdt opened this issue 3 years ago • 8 comments

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

gabrielhdt avatar May 19 '21 08:05 gabrielhdt

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

fblanqui avatar May 20 '21 09:05 fblanqui

The assert false is line 340.

fblanqui avatar May 20 '21 09:05 fblanqui

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

gabrielhdt avatar May 20 '21 09:05 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?

fblanqui avatar May 20 '21 09:05 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?

Rather than using a fatal?

gabrielhdt avatar May 20 '21 09:05 gabrielhdt

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

fblanqui avatar May 20 '21 11:05 fblanqui

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

fblanqui avatar Dec 15 '21 16:12 fblanqui