Stream: Dune devs & users

Topic: [laodpath] Coqdep vs. Coqmod


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:49):

That's what I call "loadpath" resolution

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 13:49):

Shall we start a different thread for loadpath resolution?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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/ ?

view this post on Zulip 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 ?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:52):

Yes, Dune uses coqdep, of course!

view this post on Zulip 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"?

view this post on Zulip 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)

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:56):

You do not need to match against the -Q options

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:56):

From mathcomp Require ... works

view this post on Zulip Ali Caglayan (Jun 12 2022 at 13:56):

even though there is never a -Q asdf mathcomp

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:56):

agreed

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:57):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:57):

If so there is indeed a -Q

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:57):

(and that's different from what I quoted)

view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:57):

Coq adds -Q $user_contrib ""

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 13:57):

so yes there is still a match

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 13:59):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:01):

the actual scheme is more complex

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:02):

as of today, with coq_makefile

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:02):

what is passed at build time

view this post on Zulip 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

view this post on Zulip 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 ""

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:02):

that's a mess :(

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:03):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:03):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:03):

but indeed just a spec can work too

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:04):

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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:04):

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

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:04):

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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:04):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:05):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:06):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:06):

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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:06):

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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:06):

but loadpath doesn't need -rectypes right?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:06):

Paolo Giarrusso said:

but loadpath doesn't need -rectypes right?

it does not

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:07):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:07):

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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:07):

In which case that is OK.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:07):

yes that is Ok

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:07):

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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:08):

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

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:08):

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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:08):

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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:08):

Which agrees with coqc AFAIK

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)
*)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:11):

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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:11):

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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:11):

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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:12):

extra possible requirement:

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:12):

@Rudi Grinberg yes

view this post on Zulip 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? :)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:12):

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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:13):

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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:14):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:15):

Coq has two modes:

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:16):

Ok so "regular" is just wrong with dune.

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:16):

So only boot can work correctly

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:17):

what problem you see?

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:17):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:17):

It is indeed not a huge difference

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:18):

if you follow the current model

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:20):

not it does track the deps

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:20):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:22):

I mean, clearly something cheats today, no?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:23):

Yep

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:23):

Yes

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:23):

Tho now, thanks to the composition PR we are safer

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

Dune will fail instead of indeed missing deps as before

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:24):

Still not safe enough

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:24):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

I think

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

as it is implicit

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

big problem there is the use of -R tho

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:24):

that really complicates things

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:24):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:25):

yes @Paolo Giarrusso

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:25):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:28):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:28):

Yes @Rudi Grinberg

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:29):

That's not what we are talking about tho

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:30):

from user-contrib + load path

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:30):

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

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:31):

what's "+ load path"?

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:31):

COQPATH or COQLIB?

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:31):

I only know about the second

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:33):

COQPATH

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:33):

COQLIB tells where lib/coq is

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:34):

so once COQLIB has been determined, then two things happen

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:35):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:35):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:35):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:35):

like the XDG stuff

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 14:35):

and coqrc

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:36):

yes, forget about XDG

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:36):

where should dune install stuff when COQPATH is set?

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:36):

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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:39):

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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:39):

But I also don't know for certain

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:41):

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

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:42):

@Ali Caglayan @Paolo Giarrusso one of you is wrong

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:42):

no, I think we agree

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:42):

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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:42):

what's the difference?

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:42):

I'd bet I'm wrong :-)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:43):

AFAIK COQPATH is handled just like an extra user-contrib

view this post on Zulip 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 :)

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:44):

I'd like a confirmation on this COQPATH business

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:44):

COQPATH is just "user-contrib" right?

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:44):

I can add stuff to the COQPATH environment variable

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:44):

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

view this post on Zulip 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

view this post on Zulip 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
    }

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:48):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:49):

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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:49):

This lets you "install" coq libraries wherever you want

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:50):

Wait, Emilio said that COQLIB is not user-contrib

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 14:51):

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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:51):

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:51):

user-contrib is deduced from COQLIB in the code

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:52):

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

view this post on Zulip Ali Caglayan (Jun 12 2022 at 14:52):

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

view this post on Zulip Rudi Grinberg (Jun 12 2022 at 14:52):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 15:22):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 15:24):

Indeed that's yet another problem how to handle it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 12 2022 at 15:24):

because Nix packages don't user user-contrib

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rodolphe Lepigre (Jun 12 2022 at 18:28):

And install also both ways to ensure cross-compatibility.

view this post on Zulip 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: Jan 30 2023 at 19:04 UTC