search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
265 stars 35 forks source link

dune build fails after dune clean #983

Closed fblanqui closed 7 months ago

fblanqui commented 1 year ago 
File "tests/regressions/dune", line 2, characters 16-22:
2 |  (names hrs xtc dtrees)
                    ^^^^^^
Fatal error: exception Common.Error.Fatal(0, "/home/claudio/ricerca/dedukti/lambdapi.csc/_build/default/tests/OK/boolean.lp cannot be mapped under the library root.\nConsider adding a package file under your source tree, or use the [--map-dir] option.")
File "tests/regressions/dune", line 2, characters 8-11:
2 |  (names hrs xtc dtrees)
            ^^^
Fatal error: exception Common.Error.Fatal(0, "/home/claudio/ricerca/dedukti/lambdapi.csc/_build/default/tests/OK/boolean.lp cannot be mapped under the library root.\nConsider adding a package file under your source tree, or use the [--map-dir] option.")
File "tests/regressions/dune", line 2, characters 12-15:
2 |  (names hrs xtc dtrees)
                ^^^
Fatal error: exception Common.Error.Fatal(0, "/home/claudio/ricerca/dedukti/lambdapi.csc/_build/default/tests/OK/boolean.lp cannot be mapped under the library root.\nConsider adding a package file under your source tree, or use the [--map-dir] option.")
fblanqui commented 1 year ago

hopefully, it works again after make tests

ejgallego commented 1 year ago

Seems like a missing dependency on the package file, so dune goes and executes the test without the required file being in place. Later on this file is copied so things work.