Stream: Dune devs & users

Topic: [laodpath] Coqdep vs. Coqmod

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:49):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

Gaëtan Gilbert said:

Emilio Jesús Gallego Arias said:

In Coq for example, someone thought that having 3 different implementations of loadpath resolution was a good idea

coqc/coqdep/??? what's the 3rd?

coqchk and coqdoc :S

Perhaps what is missing here is a standard rather than a single implementation. The fact that there's 3 different wrappers around walking the file system is not what's scaring me. It's that nobody knows when is one of them is incorrect.

Yes, only thing we need to agree is actually a function from Mod.*.Bar to a filename, provided the set of -Q bindings.

Paolo Giarrusso (Jun 12 2022 at 13:49):

on a technical question:

If coqmod reports From X Require A, then Dune will need to do a resolution of X and then search for A.

how true is this? I think today that's not remotely true, right?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:49):

That's what I call "loadpath" resolution

Rudi Grinberg (Jun 12 2022 at 13:49):

Shall we start a different thread for loadpath resolution?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:49):

Paolo Giarrusso said:

on a technical question:

If coqmod reports From X Require A, then Dune will need to do a resolution of X and then search for A.

how true is this? I think today that's not remotely true, right?

today Dune uses coqmod which already does the resolution itself, so we pass it -Q flags

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:50):

Rudi Grinberg said:

Shall we start a different thread for loadpath resolution?

sounds good

Rudi Grinberg (Jun 12 2022 at 13:50):

Perhaps you can describe us what the problem is and what reusable tool is available inside coq that we can use in dune?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:50):

it is actually not complex, that's why I'm suggesting to make a small common lib

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:51):

let's make a thread, but indeed the main problem is that due to historical reasons, the resolution was not really specified, and Coq used to do very weird things, for example, when an ambiogous path was found, Coq would pick a random module.

Rudi Grinberg (Jun 12 2022 at 13:51):

Emilio Jesús Gallego Arias said:

it is actually not complex, that's why I'm suggesting to make a small common lib

I'm sure you'd write it down here, if only there was enough space on the margin :)

Gaëtan Gilbert (Jun 12 2022 at 13:51):

Emilio Jesús Gallego Arias said:

Paolo Giarrusso said:

on a technical question:

If coqmod reports From X Require A, then Dune will need to do a resolution of X and then search for A.

how true is this? I think today that's not remotely true, right?

today Dune uses coqmod which already does the resolution itself, so we pass it -Q flags

s/coqmod/coqdep/ ?

Paolo Giarrusso (Jun 12 2022 at 13:51):

maybe somebody should split this — starting from https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users/topic/Coqdep.20vs.2E.20Coqmod/near/285843713 ?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:52):

Yes, Dune uses coqdep, of course!

Paolo Giarrusso (Jun 12 2022 at 13:52):

IIUC, the current semantics is not what I quoted from Ali but "for From X Require A match X.*.A against the -Q options, and X can be longer or shorter than a -Q prefix"?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:54):

(by the way, typical problems of loadpath resolution were stuff like this https://github.com/coq/coq/issues/9080)

Ali Caglayan (Jun 12 2022 at 13:56):

You do not need to match against the -Q options

Ali Caglayan (Jun 12 2022 at 13:56):

From mathcomp Require ... works

Ali Caglayan (Jun 12 2022 at 13:56):

even though there is never a -Q asdf mathcomp

Paolo Giarrusso (Jun 12 2022 at 13:56):

agreed

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:57):

That works when mathcomp is in user-contrib you mean?

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:57):

If so there is indeed a -Q

Paolo Giarrusso (Jun 12 2022 at 13:57):

(and that's different from what I quoted)

Paolo Giarrusso (Jun 12 2022 at 13:57):

the manual is even somewhat clear (https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.From-%E2%80%A6-Require)

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:57):

Coq adds -Q $user_contrib ""

Emilio Jesús Gallego Arias (Jun 12 2022 at 13:57):

so yes there is still a match

Paolo Giarrusso (Jun 12 2022 at 13:57):

the point is, nobody should expect From's argument to match _exactly_ a theory name or a -Q prefix

Ali Caglayan (Jun 12 2022 at 13:58):

But what typically gets passed to coqc is not -Q adsf mathcomp but -Q asdf/algebra mathcomp.algebra

Paolo Giarrusso (Jun 12 2022 at 13:59):

the reverse also happens — -Q asdf/algebra mathcomp.algebra and From mathcomp.algebra.foo.bar Require ...

Paolo Giarrusso (Jun 12 2022 at 14:00):

the scheme Ali had propose would be much easier to reimplement in dune:

If coqmod reports From X Require A, then Dune will need to do a resolution of X and then search for A.

Paolo Giarrusso (Jun 12 2022 at 14:00):

(and maybe coq should migrate to that scheme, but I'd strongly ask for an incremental migration strategy)

Paolo Giarrusso (Jun 12 2022 at 14:01):

the actual scheme is more complex

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:01):

Ali Caglayan said:

But what typically gets passed to coqc is not -Q adsf mathcomp but -Q asdf/algebra mathcomp.algebra

Unfortunately what is passed to coq is not stable :S

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:02):

we may want to fix that, that is an example of what we could improve

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:02):

as of today, with coq_makefile

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:02):

what is passed at build time

Paolo Giarrusso (Jun 12 2022 at 14:02):

I imagine what dune needs is that the loadpath library was designed to let you share the filesystem scan across multiple dependency resolutions

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:02):

is not the same than once is installed, where coqc passes implicity -Q $user_contrib ""

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:02):

that's a mess :(

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:03):

@Paolo Giarrusso actually Rudi is right, maybe we don't even need a common library, but just a spec

Rudi Grinberg (Jun 12 2022 at 14:03):

How do you plan your loadpath library to work with dune's Memo?

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:03):

but we don't have a complete spec, far from it

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:03):

Rudi Grinberg said:

How do you plan your loadpath library to work with dune's Memo?

we can make it take a functor

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:03):

but indeed just a spec can work too

Paolo Giarrusso (Jun 12 2022 at 14:04):

but a reimplementable spec requires fixing the semantics, while a library allows more evolution?

Paolo Giarrusso (Jun 12 2022 at 14:04):

isn't all that dune needs "share the filesystem scan"?

Rudi Grinberg (Jun 12 2022 at 14:04):

Either works for me. But if it's a library, it cannot have any other dependencies.

Ali Caglayan (Jun 12 2022 at 14:04):

I am also certain that we need to cleanup -rectypes coq side.

Rudi Grinberg (Jun 12 2022 at 14:04):

Paolo Giarrusso said:

isn't all that dune needs "share the filesystem scan"?

in dune, all code that observes the file system needs to go through our Memo monad

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:05):

Rudi Grinberg said:

Either works for me. But if it's a library, it cannot have any other dependencies.

yes, the idea is to make it standalone

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:05):

there is already a PR, but I didn't get too far

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:05):

we didn't figure out how to actually share the representation of coq module names

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:05):

Ali Caglayan said:

I am also certain that we need to cleanup -rectypes coq side.

for this work to happen? Why?

Paolo Giarrusso (Jun 12 2022 at 14:06):

@Rudi Grinberg ah, so you want Memo to handle the caching, not loadpath — I can imagine that'll be fun

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:06):

when we vendor the top-level Coq flags don't apply

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:06):

loadpath just handles the matching, provided the bindings and the FS contents

Ali Caglayan (Jun 12 2022 at 14:06):

You can't link -rectypes libraries without also assuming -rectypes.

Paolo Giarrusso (Jun 12 2022 at 14:06):

but loadpath doesn't need -rectypes right?

Rudi Grinberg (Jun 12 2022 at 14:06):

Paolo Giarrusso said:

Rudi Grinberg ah, so you want Memo to handle the caching, not loadpath — I can imagine that'll be fun

No, it's for the watch mode. Dune adds watches transparently behind file system accesses.

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:06):

Paolo Giarrusso said:

but loadpath doesn't need -rectypes right?

it does not

Ali Caglayan (Jun 12 2022 at 14:06):

Paolo Giarrusso said:

but loadpath doesn't need -rectypes right?

Right, but globally in Coq it is assumed.

Ali Caglayan (Jun 12 2022 at 14:07):

Which is why I am saying it need to be cleaned up.

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:07):

@Ali Caglayan if we do a library for this, the idea is Dune and Coq vendor it

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:07):

so that flag doesn't apply, as @Paolo Giarrusso notes

Ali Caglayan (Jun 12 2022 at 14:07):

In which case that is OK.

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:07):

yes that is Ok

Ali Caglayan (Jun 12 2022 at 14:07):

A little strange for Coq to vendor it's own loadpath lib tho

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:07):

we can do a lib, or a spec, whatever we want, we just need a way to keep it in sync

Paolo Giarrusso (Jun 12 2022 at 14:08):

@Emilio Jesús Gallego Arias is the filesystem scan done eagerly, or should it be lazy?

Rudi Grinberg (Jun 12 2022 at 14:08):

I'd say start with a spec. To make sure all the users agree on it

Ali Caglayan (Jun 12 2022 at 14:08):

There is already somewhat of a spec in the tests/source for coqdep

Ali Caglayan (Jun 12 2022 at 14:08):

Which agrees with coqc AFAIK

Rudi Grinberg (Jun 12 2022 at 14:08):

Paolo Giarrusso said:

Emilio Jesús Gallego Arias is the filesystem scan done eagerly, or should it be lazy?

It should be flexible enough to allow implementations to decide I hope

Rudi Grinberg (Jun 12 2022 at 14:09):

Ali Caglayan said:

There is already somewhat of a spec in the tests/source for coqdep

I mean a document that is readable to the users of coq

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:09):

Ali Caglayan said:

A little strange for Coq to vendor it's own loadpath lib tho

That's a component that UIs and build system are interested tho, they can link to it too, or just vendor, at will, as soon as the source code is in some place. How to organize Coq is an interesting subject, actually I would develop all this logic independently of Coq's main repos.

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:09):

Paolo Giarrusso said:

Emilio Jesús Gallego Arias is the filesystem scan done eagerly, or should it be lazy?

You wanna be lazy

Paolo Giarrusso (Jun 12 2022 at 14:09):

@Rudi Grinberg AFAICS this is the spec for Coq >= 8.15, older versions do different stuff https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.From-%E2%80%A6-Require

Ali Caglayan (Jun 12 2022 at 14:10):

This is the best doc we have today:

(** Visit all the directories under [dir], including [dir], in the
    same order as for [coqc]/[coqtop] in [System.all_subdirs], that
    is, assuming Sys.readdir to have this structure:
    ├── B
    │   └── E.v
    │   └── C1
    │   │   └── E.v
    │   │   └── D1
    │   │       └── E.v
    │   │   └── F.v
    │   │   └── D2
    │   │       └── E.v
    │   │   └── G.v
    │   └── F.v
    │   └── C2
    │   │   └── E.v
    │   │   └── D1
    │   │       └── E.v
    │   │   └── F.v
    │   │   └── D2
    │   │       └── E.v
    │   │   └── G.v
    │   └── G.v
    it goes in this (reverse) order:
    B.C2.D1.E, B.C2.D2.E,
    B.C2.E, B.C2.F, B.C2.G
    B.C1.D1.E, B.C1.D2.E,
    B.C1.E, B.C1.F, B.C1.G,
    B.E, B.F, B.G,
    (see discussion at PR #14718)
*)

Paolo Giarrusso (Jun 12 2022 at 14:10):

then the cache for filesystem access needs to be lazy (and hide mutation) and behave purely functionally (result of one resolution don't affect another one)

Rudi Grinberg (Jun 12 2022 at 14:10):

Paolo Giarrusso said:

Rudi Grinberg AFAICS this is the spec for Coq >= 8.15, older versions do different stuff https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.From-%E2%80%A6-Require

that doesn't mention user-contrib.

Paolo Giarrusso (Jun 12 2022 at 14:11):

@Rudi Grinberg that's in the link to https://coq.inria.fr/refman/language/core/modules.html#libraries-and-filesystem

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:11):

Well spotted @Paolo Giarrusso , that was much improved in 8.15! Tho I bet the code still doesn't fully conform

Paolo Giarrusso (Jun 12 2022 at 14:11):

I've just noticed Hugo's MR :-)

Rudi Grinberg (Jun 12 2022 at 14:11):

the directories listed in the $COQPATH, ${XDG_DATA_HOME}/coq/ and ${XDG_DATA_DIRS}/coq/ environment variables (see XDG base directory specification) with the same physical-to-logical translation and with an empty logical prefix.

Is this true for any implementation today?

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:11):

@Rudi Grinberg user-contrib and COQPATH are handled by doing -Q $user_contrib ""

Paolo Giarrusso (Jun 12 2022 at 14:11):

I hadn't realized it came with good docs but it's not surprising

Paolo Giarrusso (Jun 12 2022 at 14:12):

extra possible requirement:

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:12):

Yes I was aware of Hugo's PR but didn't know he improved the docs so much

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:12):

@Rudi Grinberg yes

Gaëtan Gilbert (Jun 12 2022 at 14:12):

Rudi Grinberg said:

Ali Caglayan said:

There is already somewhat of a spec in the tests/source for coqdep

I mean a document that is readable to the users of coq

so a .v file? :)

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:12):

tho older Coq versions will be maybe buggier, but we don't really care IMHO

Paolo Giarrusso (Jun 12 2022 at 14:12):

for IDE tooling, I might want (the option) to share the FS cache across projects

Paolo Giarrusso (Jun 12 2022 at 14:13):

that is, the FS cache should not know the -Q options

Rudi Grinberg (Jun 12 2022 at 14:14):

Emilio Jesús Gallego Arias said:

Rudi Grinberg user-contrib and COQPATH are handled by doing -Q $user_contrib ""

Could you clarify the handling? Is that what dune should pass today for example?

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:14):

Dune doesn't need to pass it unless you use -boot

Rudi Grinberg (Jun 12 2022 at 14:14):

Paolo Giarrusso said:

for IDE tooling, I might want (the option) to share the FS cache across projects

connect to dune via rpc, and do your FS accesses via dune

Rudi Grinberg (Jun 12 2022 at 14:14):

Emilio Jesús Gallego Arias said:

Dune doesn't need to pass it unless you use -boot

I think we decided that -boot is the good default, right?

Paolo Giarrusso (Jun 12 2022 at 14:15):

@Rudi Grinberg but dune can only do it if the FS cache doesn't depend on -Q

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:15):

Coq has two modes:

• boot : nothing is added, so indeed you need to add even the -Q with empty prefix (that will just scan the directory given and build the map)
• regular: coq tries to detect where the standard library is, then it will add -R $stdlib Coq -Q $user_contrib "" and the other stuff documented. The user-contrib dir is determined from the stdlib path

Rudi Grinberg (Jun 12 2022 at 14:16):

Ok so "regular" is just wrong with dune.

Rudi Grinberg (Jun 12 2022 at 14:16):

So only boot can work correctly

Paolo Giarrusso (Jun 12 2022 at 14:16):

I only say that because some obvious designs don't achieve this property, and this is easy to ensure when redesigning the API and painful to fix later

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:16):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

Dune doesn't need to pass it unless you use -boot

I think we decided that -boot is the good default, right?

For 2.0 version yes, for 1.0 we could indeed try, but we need more work on dune side.

Ali Caglayan (Jun 12 2022 at 14:16):

Emilio Jesús Gallego Arias said:

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

Dune doesn't need to pass it unless you use -boot

I think we decided that -boot is the good default, right?

For 2.0 version yes, for 1.0 we could indeed try, but we need more work on dune side.

I claim that we can do this for version 1.0 without breaking anything.

Rudi Grinberg (Jun 12 2022 at 14:16):

We can support both modes for all i care. it's really not a huge a difference

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:17):

Rudi Grinberg said:

So only boot can work correctly

regular can also work, you just need to handle the implicit -Q

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:17):

what problem you see?

Paolo Giarrusso (Jun 12 2022 at 14:17):

(e.g. mkLoadPathCache : LoadPathOptions -> LoadPathCache would be bad, but I'll stop here)

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:17):

It is indeed not a huge difference

Rudi Grinberg (Jun 12 2022 at 14:17):

Emilio Jesús Gallego Arias said:

Rudi Grinberg said:

So only boot can work correctly

regular can also work, you just need to handle the implicit -Q

we need to tell dune that coqc commands without -boot all depend on user-contrib

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:17):

in both cases, for 1.0 model, we need to support the empty prefix

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:18):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

Rudi Grinberg said:

So only boot can work correctly

regular can also work, you just need to handle the implicit -Q

we need to tell dune that coqc commands without -boot all depend on user-contrib

yes, that's what installed_theories db should do

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:18):

if you follow the current model

Rudi Grinberg (Jun 12 2022 at 14:18):

Ok but today it doesn't do it. So the rules without -boot are incorrect. At least from dune's perspective

Paolo Giarrusso (Jun 12 2022 at 14:19):

@Rudi Grinberg if you add the user-contrib dependency, the entire cache would be invalidated at any package installation/removal, right?

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:20):

@Rudi Grinberg indeed, as of today, Dune doesn't work when a (theory ...) is present in user-contrib

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:20):

not it does track the deps

Paolo Giarrusso (Jun 12 2022 at 14:20):

that's indeed required today for sound caching, but I'm sure @Emilio Jesús Gallego Arias knew that when he wrote today's code

Rudi Grinberg (Jun 12 2022 at 14:20):

Paolo Giarrusso said:

Rudi Grinberg if you add the user-contrib dependency, the entire cache would be invalidated at any package installation/removal, right?

Yes, watchers would notify some directories are out of date and the stat cache for them would be blown off in dune

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:20):

Not sure if at any, we can track the deps more precisely actually

Paolo Giarrusso (Jun 12 2022 at 14:21):

@Rudi Grinberg I rather meant that all compiled .vo would not be usable any more... but maybe it is just the .v.d files?

Rudi Grinberg (Jun 12 2022 at 14:21):

Paolo Giarrusso said:

that's indeed required today for sound caching, but I'm sure Emilio Jesús Gallego Arias knew that when he wrote today's code

dont worry about caching. if you use dune's api you will be automatically correct here

Paolo Giarrusso (Jun 12 2022 at 14:22):

I mean, clearly something cheats today, no?

Rudi Grinberg (Jun 12 2022 at 14:22):

we have two rules of discipline:

1. always specify the deps your build rules
2. always observe the fs through the memo api

that's enough for correctness in watch mode

Rudi Grinberg (Jun 12 2022 at 14:23):

Paolo Giarrusso said:

Rudi Grinberg I rather meant that all compiled .vo would not be usable any more... but maybe it is just the .v.d files?

if their hashes changed, sure they would be invalided.

Paolo Giarrusso (Jun 12 2022 at 14:23):

I just mean coqc will read files from user-contrib that coqdep doesn't declare dependencies on?

Ali Caglayan (Jun 12 2022 at 14:23):

Yep

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:23):

Yes

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:23):

Tho now, thanks to the composition PR we are safer

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

Dune will fail instead of indeed missing deps as before

Ali Caglayan (Jun 12 2022 at 14:24):

Still not safe enough

Rudi Grinberg (Jun 12 2022 at 14:24):

To be "safe" today, we need to always -boot

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

Only unsafe w.r.t. Coq's stdlib

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

I think

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

as it is implicit

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

big problem there is the use of -R tho

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

that really complicates things

Paolo Giarrusso (Jun 12 2022 at 14:24):

at least before composition, it was unsafe wrt the entire user-contrib, right?

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:25):

we go back to the point I made the other day, when I released jsCoq I required everyone to do From Coq Require .... for using the stdlib

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:25):

yes @Paolo Giarrusso

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:25):

now it is also unsafe if you don't specify theories correctly

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:26):

there are these interesting build systems that actually strace a process and add as a dep every file accessed hehe

Ali Caglayan (Jun 12 2022 at 14:27):

Emilio Jesús Gallego Arias said:

there are these interesting build systems that actually strace a process and add as a dep every file accessed hehe

Adding dependencies after stracing coqc seems like the wrong way round no?

Rudi Grinberg (Jun 12 2022 at 14:28):

Ali Caglayan said:

Emilio Jesús Gallego Arias said:

there are these interesting build systems that actually strace a process and add as a dep every file accessed hehe

Adding dependencies after stracing coqc seems like the wrong way round no?

it's not wrong, but it does have disadvantages. It's like an automatic dap mode though

Paolo Giarrusso (Jun 12 2022 at 14:28):

I thought bazel rather sandboxed the build, exposing only declared dependencies

Rudi Grinberg (Jun 12 2022 at 14:28):

I think it will be useful to split the discussion in two ways:

1. what is required to support user-contrib today
2. what should a proper load path solution look like

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:28):

That's the dual of sandboxing in a sense, you can do that and then complain if the user didn't declare the deps

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:28):

Yes @Rudi Grinberg

Paolo Giarrusso (Jun 12 2022 at 14:29):

to be sure, looking at composition's docs in https://github.com/ocaml/dune/pull/5784, theories cannot list installed libraries yet, right? That MR is great tho

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:29):

I propose we discuss 1 on this thread, and create a new one for the "new model" where, every library has to be build with dune

Ali Caglayan (Jun 12 2022 at 14:29):

That's not what we are talking about tho

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:29):

so for 1. I think what we need to do is to build a DB installed_theories

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:30):

from user-contrib + load path

Ali Caglayan (Jun 12 2022 at 14:30):

user-contrib + loadpath shouldn't need whatever is in there to be built by dune

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:30):

and condition the notion of soundness to the actual soundness of the installed_theories DB

Rudi Grinberg (Jun 12 2022 at 14:31):

what's "+ load path"?

Rudi Grinberg (Jun 12 2022 at 14:31):

COQPATH or COQLIB?

Ali Caglayan (Jun 12 2022 at 14:31):

I only know about the second

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:33):

COQPATH

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:33):

COQLIB tells where lib/coq is

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:34):

so the effective path is COQLIB (if present, otherwise value chosen at configure time, or by the -coqlib cmdline option) + COQPATH

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:34):

so once COQLIB has been determined, then two things happen

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:35):

-R $COQLIB/theories Coq and -Q $COQLIB/user-contrib ""

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:35):

plus for each additional path in COQPATH, we do -Q $PATH ""

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:35):

the rest of cases are highly anecdoticla and could be actually deprecated

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:35):

like the XDG stuff

Emilio Jesús Gallego Arias (Jun 12 2022 at 14:35):

and coqrc

Rudi Grinberg (Jun 12 2022 at 14:36):

yes, forget about XDG

Rudi Grinberg (Jun 12 2022 at 14:36):

where should dune install stuff when COQPATH is set?

Rudi Grinberg (Jun 12 2022 at 14:36):

btw, do coq's makefiles support this COQPATH/COQLIB business at all?

Ali Caglayan (Jun 12 2022 at 14:39):

coqdep and coqc know about "COQPATH", AFAIK coq_makefile doesn't do anything with it

Ali Caglayan (Jun 12 2022 at 14:39):

But I also don't know for certain

Rudi Grinberg (Jun 12 2022 at 14:41):

then what's the point of us supporting COQPATH? if the legacy stuff doesn't put anything there, we gain nothing by reading from it

Paolo Giarrusso (Jun 12 2022 at 14:41):

the legacy stuff reads from it, it just does not track dependencies

Rudi Grinberg (Jun 12 2022 at 14:42):

@Ali Caglayan @Paolo Giarrusso one of you is wrong

Paolo Giarrusso (Jun 12 2022 at 14:42):

no, I think we agree

Ali Caglayan (Jun 12 2022 at 14:42):

I'm willing to bet it is me who is wrong :)

Paolo Giarrusso (Jun 12 2022 at 14:42):

what's the difference?

Paolo Giarrusso (Jun 12 2022 at 14:42):

I'd bet I'm wrong :-)

Paolo Giarrusso (Jun 12 2022 at 14:43):

but if you're claiming that coqdep will track dependencies from COQPATH correctly, I think I've tried that out and it doesn't

Paolo Giarrusso (Jun 12 2022 at 14:43):

AFAIK COQPATH is handled just like an extra user-contrib

Rudi Grinberg (Jun 12 2022 at 14:43):

Paolo Giarrusso said:

but if you're claiming that coqdep will track dependencies from COQPATH correctly, I think I've tried that out and it doesn't

That's not a bad thing. Dependency analysis shouldn't climb the file system arbitrarily :)

Rudi Grinberg (Jun 12 2022 at 14:44):

I'd like a confirmation on this COQPATH business

Ali Caglayan (Jun 12 2022 at 14:44):

COQPATH is just "user-contrib" right?

Paolo Giarrusso (Jun 12 2022 at 14:44):

I can add stuff to the COQPATH environment variable

Ali Caglayan (Jun 12 2022 at 14:44):

Then when Emilio say COQLIB + COQPATH does this mean "lib/coq" + "user-contrib"?

Paolo Giarrusso (Jun 12 2022 at 14:45):

_however_, _I_ do this seldom, and could use dune instead... OTOH somebody should check what Nix does

Ali Caglayan (Jun 12 2022 at 14:47):

Nix:

  setupHook = writeText "setupHook.sh" "
    addCoqPath () {
      if test -d \"$1/lib/coq/${coq-version}/user-contrib\"; then
        export COQPATH=\"\${COQPATH-}\${COQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\"
      fi
    }

Paolo Giarrusso (Jun 12 2022 at 14:48):

and documented in https://nixos.wiki/wiki/Coq etc

Paolo Giarrusso (Jun 12 2022 at 14:49):

so Nix doesn't have a global user-contrib, but it has one per each Nix library package, and lists them in COQPATH

Ali Caglayan (Jun 12 2022 at 14:49):

(** Standard LoadPath for Coq user libraries; in particular it
   includes (in-order) Coq's standard library, Coq's [user-contrib]
   folder, and directories specified in [COQPATH] and [XDG_DIRS] *)
val init_load_path
  : coqenv:Boot.Env.t
  -> CUnix.physical_path list * Loadpath.vo_path list

Ali Caglayan (Jun 12 2022 at 14:49):

OK so COQPATH is done in addition to COQLIB (which is user-contrib)

Ali Caglayan (Jun 12 2022 at 14:49):

This lets you "install" coq libraries wherever you want

Paolo Giarrusso (Jun 12 2022 at 14:50):

Wait, Emilio said that COQLIB is not user-contrib

Paolo Giarrusso (Jun 12 2022 at 14:51):

but otherwise yes, it's user-contrib + COQPATH, as I was saying

Ali Caglayan (Jun 12 2022 at 14:51):

• COQLIB = lib/coq/
• "user-contrib" = lib/coq/user-contrib
• COQPATH = whatever

Ali Caglayan (Jun 12 2022 at 14:51):

user-contrib is deduced from COQLIB in the code

Ali Caglayan (Jun 12 2022 at 14:52):

coq_makefile installs to user-contrib by default (IDK if it can be configured)

Ali Caglayan (Jun 12 2022 at 14:52):

The install rules in Dune today for Coq also install to user-contrib

Rudi Grinberg (Jun 12 2022 at 14:52):

yes, we'll install to user-contrib as well.

Rudi Grinberg (Jun 12 2022 at 14:53):

following that, we'll think of a proper installation scheme that respects dune's package loading and allows us to include metadata

Emilio Jesús Gallego Arias (Jun 12 2022 at 15:22):

COQPATH is just a way to emulate a more saner packagin setup

Emilio Jesús Gallego Arias (Jun 12 2022 at 15:24):

Indeed that's yet another problem how to handle it

Emilio Jesús Gallego Arias (Jun 12 2022 at 15:24):

because Nix packages don't user user-contrib

Emilio Jesús Gallego Arias (Jun 12 2022 at 15:24):

however we have no way to override that, I guess Nix would have to rewrite the .install files we generate :S

Rodolphe Lepigre (Jun 12 2022 at 17:40):

Rudi Grinberg said:

following that, we'll think of a proper installation scheme that respects dune's package loading and allows us to include metadata

Speaking about installation scheme, I was wondering: wouldn't it be an (fairly straight-forward) option to piggy-back on the OCaml infrastructure for installing deps? I mean, we could certainly use ocamlfind to locate Coq libraries if we installed them like ocaml packages. You could then interpret From lib_name Require some.module.path as running an ocamlfind query lib_name to search for the library path, and then search for the qualified module under that path.

We could probably make it so that coqmakefile produces an installation rule that installs under both the user-contrib and the way I propose above, for backward compatibility (at least for a while). And of course, the Coq standard library could be installed also under the appropriate path.

Is there anything I'm missing here? Because that seems like a quite a simple plan to implement, and since it already works for OCaml in dune, I don't see why it could not work (fairly trivially) for Coq.

Rodolphe Lepigre (Jun 12 2022 at 17:42):

(Of course, the suggestion above imposes a stricter discipline than what Coq allows for From ... Require ..., but I think most users would be fine sticking to this. And a sed script can probably be written to adapt projects to that discipline.)

Rudi Grinberg (Jun 12 2022 at 18:21):

@Rodolphe Lepigre that’s a simple and good scheme. It will introduce very few issues and allow dune to load externally installed packages all at once instead of partially loading them through user-contrib

Rudi Grinberg (Jun 12 2022 at 18:25):

One objection though: let’s not modify the makefile stuff. It’s much easier to just make dune understand what coq makefile is installing. Dune can install in legacy and new locations at once

Rodolphe Lepigre (Jun 12 2022 at 18:25):

A few more thoughts on that: it may be that a package installs both OCaml and Coq code, so it might be necessary to add another layer of directories for this installation scheme to work. The folder could be called coq_files or theories for example. So if ocamlfind query lib_name returns a path /path/to/library then the coq files would end up in /path/to/library/theories.

Rodolphe Lepigre (Jun 12 2022 at 18:27):

Rudi Grinberg said:

One objection though: let’s not modify the makefile stuff. It’s much easier to just make dune understand what coq makefile is installing. Dune can install in legacy and new locations at once

But that would mean that a dune project can only depend on other dune-installed projects, right? If we are clear about what the installation scheme is, it should be very easy for whoever is maintaining a Coq project not compiled with dune to install it in the way dune expects.

Rodolphe Lepigre (Jun 12 2022 at 18:28):

And install also both ways to ensure cross-compatibility.

Rudi Grinberg (Jun 13 2022 at 00:52):

dune can still read from makefile installed theories. We just don’t need to rely on that for our own theories

Last updated: Oct 13 2024 at 01:02 UTC