Deducteam / Dedukti

Implementation of the λΠ-calculus modulo rewriting
https://deducteam.github.io
Other
200 stars 22 forks source link

Path resolution #294

Closed gabrielhdt closed 1 year ago

gabrielhdt commented 2 years ago

There seem to be a recurring malfunction: paths are (always?) prepended with ./, even when they should not. For instance, assume we have three files,

D/unit.dk

Unit: Type.
unit: Unit.

D/unitLib.dk

#REQUIRE unit.
id : unit.Unit -> unit.Unit.

foo.dk

#REQUIRE unit.
#REQUIRE unitLib.
def bar := unitLib.id unit.unit.

Symptom 1: dk dep

Dependency computation returns a not-so-correct output:

$ cd D
$ dk dep *.dk
./unit.dko : unit.dk
./unitLib.dko : unitLib.dk ./unit.dko

With these dependencies, make unitLib.dko just does not work (I assume it's because unitLib.dko is not the same as ./unitLib.dko for make).

Symptom 2: dk check

Assuming D/unit.dko and D/unitLib.dko have been created, the command

$ dk check -I D/ foo.dk
[SUCCESS] foo.dk was successfully checked.

works, but

$ dk check -I "$(realpath D)" foo.dk
[ERROR CODE:902] ...
No object file (.dko) found for module unit located at .//[...]/D/unit.dko