expected relative path

[ckeller]

Hi

I would like to call lambdapi on a file which is not in a subdirectory of my working directory, say /tmp/foo.dk. However, lambdapi fails with the following error:

$ lambdapi /tmp/foo.dk 
[unknown location] Invalid path for [/tmp/foo.dk] (expected relative path).

I am using the opam package but a quick look at the master branch let me think that it would produce the same answer.

Thank you for your help.

[fblanqui]

Hello Chantal. This is on purpose. For the moment, LP does not accept file names with absolute paths. Why not running LP in /tmp, or moving your file foo.dk somewhere else?

[ckeller]

I am calling lambdapi from another tool so

• I do not control the working directory from which lambdapi is called
• I do not want to pollute the user's space

Why such a restriction?

[fblanqui]

Workaround: instead of calling LP directly, use a script that will run LP on the filename part only from the dirname part.
Why such a restriction? @rlepigre shall give you some argument soon hopefully.

[rlepigre]

The justification for this behavior is that this enforces a correspondence between file path and module path. This simplifies many things, but there are also limitations as you just discovered @ckeller. Of course, this is not satisfactory, and we need some mechanism that:

1. is more permissive,
2. retains some of the good properties we have now for the dependency analysis.

There are several options here:

1. Having a PATH-like mechanism (a list of directories to explore in order when looking for a module).
2. Introducing mappings between arbitrary directories and module path prefixes (that is what Coq does to some extend I believe, but it is not always great).

Could you please elaborate a bit on your use case @ckeller:

1. Are your Lambdapi files completely self-contained? If that is the case, then there is an easy workaround.
2. Would a PATH-like mechanism suffice for your application?

[francoisthire]

What are the issues with Coq system? I have the impression that it is always better to make the distinction between the file system and the logical path. Le jeu. 10 oct. 2019 à 22:44, Rodolphe Lepigre <[email protected]> a écrit :

…

The justification for this behavior is that this enforces a correspondence between file path and module path. This simplifies many things, but there are also limitations as you just discovered @ckeller <https://github.com/ckeller>. Of course, this is not satisfactory, and we need some mechanism that: 1. is more permissive, 2. retains some of the good properties we have now for the dependency analysis. There are several options here: 1. Having a PATH-like mechanism (a list of directories to explore in order when looking for a module). 2. Introducing mappings between arbitrary directories and module path prefixes (that is what Coq does to some extend I believe, but it is not always great). Could you please elaborate a bit on your use case @ckeller <https://github.com/ckeller>: 1. Are your Lambdapi files completely self-contained? If that is the case, then there is an easy workaround. 2. Would a PATH-like mechanism suffice for your application? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#243?email_source=notifications&email_token=AATJVK5KD337H6E3DZMI4UTQN6H37A5CNFSM4I7KSMMKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEA53RLQ#issuecomment-540784814>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AATJVK2TG243LVJSCFLLYALQN6H37ANCNFSM4I7KSMMA> .

[ckeller]

Hi @rlepigre
Thank you for the explanation.

1. Are your Lambdapi files completely self-contained? If that is the case, then there is an easy workaround.

No, the objective is to have a prelude in some directory and some other files in other directories. We can as a first step be ok with a self-contained file but not on the longer term. What would the workaround be?

2. Would a `PATH`-like mechanism suffice for your application?

Probably, see above for what we need.

[rlepigre]

What are the issues with Coq system? I have the impression that it is always better to make the distinction between the file system and the logical path.

@francoisthire the problem is that the user is responsible for doing to many things (e.g., writing a _CoqProject file). I would like to have more automation on that front (i.e., a reasonable default behaviour). For instance, given an entry point for the installed libraries (that is a path like /.../lib/lambdapi) you could then access the files in inner folders like stdlib/list.lp using the qualification stdlib.list, and similarly for matita/blabla.dk. So installing everything in that particular folder would be enough for Lambdapi to be able to find any installed file in the expected way.

[rlepigre]

We can as a first step be ok with a self-contained file but not on the longer term. What would the workaround be?

@ckeller: I'll elaborate later, but I was thinking of running the command cd dir; lambdapi file.lp instead of lambdapi dir/file.lp.

(I'm busy right now, but I'll try to come up with a solution that we could then all discuss to see if it suits everyone's need.)

[fblanqui]

This issue is a kind of duplicate of #93 . We should close one of the two.

[fblanqui]

@ckeller did you find a workaround?

[fblanqui]

@rlepigre we should really do something about that because this is the second time a user stumbles on this issue...

[ckeller]

@fblanqui For the moment, my workaround is to use dkcheck (I know, it is not going to be developed anymore). I may switch to lambdapi in the next weeks using @rlepigre trick but I admit it would be very useful to be able to call lambdapi independently from the path.

Anyway, thank you for your help and for developping lambdapi!

[fblanqui]

Hello @rlepigre . Do you think you can handle this issue soon?

[rlepigre]

Yeah, I'm gonna try to do that before the end of the month.