Lake absolute rootdir

Stream: lean4

[James Gallicchio]

Is there any particular issue with Lake giving an absolute path for the rootDir of a package? I think it would just require a handful of lines to change, mainly CliM.run in Lake/CLI/Main.lean. It would also bump the lake CLI up from BaseIO to IO, but I don't think that is a huge issue?

Motivation: I was surprised to find out the workspace rootDir was just "." after trying to use it in a context where I had changed directories. I'm just using IO.currentDir in my lakefile now.

[James Gallicchio]

(and it would be decidedly more useful if it were an absolute path IMO)

[Arthur Paulino]

That "." can change when the package is being used as a dependency... to something like "./lake-packages/<cloned pkg dir name>". To get the absolute path you can use IO.currentDir and then merge the result with what Lake already tells you. But it seems to me that you shouldn't be needed to deal with that :thinking:

[Arthur Paulino]

Can you link to the source where you're needing the absolute path?

[James Gallicchio]

Uh, sure, lemme push this to a repository

[James Gallicchio]

(basically I am revamping my CaDiCaL FFI's build stack to use lean-llvm as its toolchain, so I have a copy of lean-llvm in the root directory and i need to refer to that from within a different subdirectory.........)

[James Gallicchio]

https://github.com/JamesGallicchio/LeanSAT/blob/master/lakefile.lean#L68

[James Gallicchio]

The process I spawn has to have the cadical folder as its CWD, but it needs to also get an argument that is relative to the CWD. Better if the argument is simply an absolute path.

[Arthur Paulino]

Ah okay, you're using something completely external to the Lake pkg. In this case you indeed need the absolute path

[James Gallicchio]

I thought rootDir was the intended way to refer to stuff in the package's root directory :/

[Arthur Paulino]

@James Gallicchio idea: get that external path from an environment variable CADICAL_PATH so different people can compile your project without you having to guess where that folder is

[James Gallicchio]

That would probably work, and I could do the same for the lean-llvm dependency. But I do kind of like it being self contained and self managed :/

[James Gallicchio]

does Lake have (1) a way for downstream users to pass configuration options up, and (2) a way to get configuration information from the lakefile to the source code?

[Arthur Paulino]

James Gallicchio said:

That would probably work, and I could do the same for the lean-llvm dependency. But I do kind of like it being self contained and self managed :/

Idea 2: write that path on a text file and load it in the lakefile.lean

[James Gallicchio]

Realizing perhaps this is specific enough to this project to move to #std4 > SAT core defs in Std?...

[Arthur Paulino]

James Gallicchio said:

does Lake have (1) a way for downstream users to pass configuration options up, and (2) a way to get configuration information from the lakefile to the source code?

I don't think there is a standard way, but you can create your own config file and parse it manually. Or use a JSON file

[James Gallicchio]

Arthur Paulino said:

James Gallicchio said:

That would probably work, and I could do the same for the lean-llvm dependency. But I do kind of like it being self contained and self managed :/

Idea 2: write that path on a text file and load it in the lakefile.lean

Potentially. And then I would want the root directory of the downstream dependency's package most likely, so that users of the library don't have to dig through the lake-packages stuff to find what they want.

[Arthur Paulino]

The issue of config files is that they're not allowed to be git ignored, so others will have to change them manually and pushing their changes will potentially make it incompatible with your setup. That's why env vars are the usual way for this kind of setup to work

[Mac]

@James Gallicchio I think the main question here is how are you expecting end users (i.e., downstream dependents) to acquire and/or specify the location of the needed lean-llvm and cadical libraries?

[Mac]

From your lakefile, it appears you are expecting users to download the necessary files into the root directory of their package (or your package? -- I am not entirely clear on your intent). If so, Arthur is right, you can use IO.currentDir + the package path to get a absolute path. Alternatively, you can also use IO.FS.realPath to convert the relative path to an absolute one.

[Mac]

My rational for using an relative path is twofold: 1) there were some problems with IO.FS.realPath when I first wrote that part of Lake that I believe made it not work on all OSes at the time (I think that has since been fixed) 2) using an resolved absolute path result in different directories for relative paths like '...' in the presence of things like symlinks.

[James Gallicchio]

Totally makes sense. I'm not sure what I want to do, which is why my lakefile is a bit scuffed :sweat_smile: I think it will be resolved once I figure out how I want to handle package configuration options.