Stream: Dune devs & users

Topic: Public/Private names?

Rudi Grinberg (May 27 2022 at 14:42):

@Emilio Jesús Gallego Arias I noticed that you got rid of public names in the theory stanza. It's not an essential feature in dune, but it does have one important use on the OCaml side: whenever dune is unable to resolve a library foo or foo.bar, it knows to suggest the user to install package foo. I find this hint to be quite important for users. Especially for those that are unfamiliar with the common opam packages and what libraries they provide.

Emilio Jesús Gallego Arias (May 27 2022 at 14:43):

For Coq, that would be the only use

Emilio Jesús Gallego Arias (May 27 2022 at 14:43):

in the current mode "coq lang 1.0" there is no notion of public name, the namespace is à la Haskell, global and modules are organized A.B.C.D

Emilio Jesús Gallego Arias (May 27 2022 at 14:43):

you have the package tho

Emilio Jesús Gallego Arias (May 27 2022 at 14:44):

but yeah that doesn't help a lot

Emilio Jesús Gallego Arias (May 27 2022 at 14:44):

problem is, in the 1.0 model, pkg1.Aand pkg2.A do conflict

Rudi Grinberg (May 27 2022 at 14:44):

You could introduce a similar limitation on theory names. E.g. that theory foo must belong to package foo.

Emilio Jesús Gallego Arias (May 27 2022 at 14:44):

That would rule out all of the current Coq developments

Rudi Grinberg (May 27 2022 at 14:44):

I'm not sure how well received that may be.

Emilio Jesús Gallego Arias (May 27 2022 at 14:44):

IIUC

Emilio Jesús Gallego Arias (May 27 2022 at 14:45):

1.0 goal is to allow people to port their projects to Dune, IMHO

Emilio Jesús Gallego Arias (May 27 2022 at 14:45):

then we hope to do a 2.0 which is more principled

Rudi Grinberg (May 27 2022 at 14:45):

Ok well, then perhaps public names should make a return? Otherwise people will be stuck with randomly typing opam install commands

Emilio Jesús Gallego Arias (May 27 2022 at 14:45):

I'd be great if they could make a return, but I can't see how they'd work

Emilio Jesús Gallego Arias (May 27 2022 at 14:45):

do you have an example?

Karl Palmskog (May 27 2022 at 14:45):

the reality is that some people even use completely separate base names in the same package, e.g., a package foo can have bar.qux and qux.bar

Emilio Jesús Gallego Arias (May 27 2022 at 14:46):

I'm afraid people will be stuck with having to know what opam package to sue

Emilio Jesús Gallego Arias (May 27 2022 at 14:46):

many people don't even use opam in the coq wolrd

Rudi Grinberg (May 27 2022 at 14:46):

just to be clear, public names are going to be completely invisible to coq (like they are for OCaml)

Emilio Jesús Gallego Arias (May 27 2022 at 14:46):

what I mean is that you don't have the means to resolve them to anything meaningful

Rudi Grinberg (May 27 2022 at 14:47):

that's just a matter of populating dune-package metadata, no?

Emilio Jesús Gallego Arias (May 27 2022 at 14:47):

and they create a critical ambiguitiy, so that seems more of a misfeature to me

Emilio Jesús Gallego Arias (May 27 2022 at 14:47):

1.0 has to work with non-dunerized libs

Emilio Jesús Gallego Arias (May 27 2022 at 14:48):

I think 2.0 requires both more metadata and changes in Coq

Rudi Grinberg (May 27 2022 at 14:48):

When you say non-dunerized libs, in which direction do you mean:

1. dune projects can consume coq makefile theories
2. coq makefile theories can consume dune theories

Emilio Jesús Gallego Arias (May 27 2022 at 14:49):

1

Emilio Jesús Gallego Arias (May 27 2022 at 14:49):

and also 2. would be good, but that's less important, tho yes they can consume them as we keep the current layout for now

Rudi Grinberg (May 27 2022 at 14:50):

ok, then I don't see the problem. dune would install things in a way that makefile projects understand things. But when you use installed dune theories in other dune projects, you should use the public names.

Emilio Jesús Gallego Arias (May 27 2022 at 14:51):

how do you declare a dep from a dunerized Coq project to a non-dunerized one?

Emilio Jesús Gallego Arias (May 27 2022 at 14:51):

how is (theories pkg1.A pkg2.A) resolved?

Rudi Grinberg (May 27 2022 at 14:53):

1. Look up pkg1's dune-project

2. If the dune-project exists:

   - Check if A is the list of defined theories
   - If yes, use it. If no, complain that pkg1 doesn't have the theory

3. If it doesn't, use the fallback lookup for non-dunerized projects

Emilio Jesús Gallego Arias (May 27 2022 at 14:54):

what does 2 do that 3 doesn't?

Emilio Jesús Gallego Arias (May 27 2022 at 14:54):

we already do that

Emilio Jesús Gallego Arias (May 27 2022 at 14:54):

keep in mind that all coq theories are dumped together in user-contrib

Emilio Jesús Gallego Arias (May 27 2022 at 14:55):

in the 1.0, so indeed, other than for an opam hint, public_name is not useful

Rudi Grinberg (May 27 2022 at 14:55):

I suppose I missed the 4th. step. If both look ups fail, we can suggest the user to install pkg1 which seems like a useful hint.

Emilio Jesús Gallego Arias (May 27 2022 at 14:55):

you didn't consider the real problem up there, which is what to do with pkg2

Emilio Jesús Gallego Arias (May 27 2022 at 14:55):

as it is in conflict with pkg1

Emilio Jesús Gallego Arias (May 27 2022 at 14:56):

in the OCaml world, different packages go to different directories, this is not the case (yet) in Coq

Rudi Grinberg (May 27 2022 at 14:56):

Isn't that coqc's job though? To say that the conflict exists

Emilio Jesús Gallego Arias (May 27 2022 at 14:56):

so you lack injectivity of public names to locations and that's IMHO a dangerous thing

Rudi Grinberg (May 27 2022 at 14:57):

In OCaml, there's a similar problem with unwrapped libraries. One can try to use libraries that provide overlapping names but ocamlc will complain

Emilio Jesús Gallego Arias (May 27 2022 at 14:57):

but you still can solve it using -I

Paolo Giarrusso (May 27 2022 at 14:57):

sorry, isn't there a bigger problem? opam cannot help with unsatisfied deps in (theories pkg1.A pkg2.A)...

Emilio Jesús Gallego Arias (May 27 2022 at 14:57):

in Coq, once you are there, you are boom

Emilio Jesús Gallego Arias (May 27 2022 at 14:57):

as both map to the same filesystem location

Paolo Giarrusso (May 27 2022 at 14:57):

so you're talking of a future world where that's fixed, not of the present?

Emilio Jesús Gallego Arias (May 27 2022 at 14:57):

I'm talking about the present

Emilio Jesús Gallego Arias (May 27 2022 at 14:58):

in a future world, it is very clear that as the very minium, a coq package should install in lib/coq/$pkg

Rudi Grinberg (May 27 2022 at 14:58):

Paolo Giarrusso said:

sorry, isn't there a bigger problem? opam cannot help with unsatisfied deps in (theories pkg1.A pkg2.A)...

yes, it can't help, but we want to design things so that it can help

Emilio Jesús Gallego Arias (May 27 2022 at 14:58):

not in lib/coq/user-contrib

Rudi Grinberg (May 27 2022 at 14:58):

Emilio Jesús Gallego Arias said:

in a future world, it is very clear that as the very minium, a coq package should install in lib/coq/$pkg

Yes, that's obviously much better.

Emilio Jesús Gallego Arias (May 27 2022 at 14:59):

Rudi Grinberg said:

Paolo Giarrusso said:

sorry, isn't there a bigger problem? opam cannot help with unsatisfied deps in (theories pkg1.A pkg2.A)...

yes, it can't help, but we want to design things so that it can help

I'm afraid that as two packages can provide the same lib/coq/user-contrib/A.v file, it is not possible to make this work well with the current lib model

Rudi Grinberg (May 27 2022 at 14:59):

Why can't we do that right away with dune? In other words, install to two locations:

1. user-contrib for compatibility
   2.lib/coq/$pkg as well

Emilio Jesús Gallego Arias (May 27 2022 at 14:59):

Yes, that's the goal

Emilio Jesús Gallego Arias (May 27 2022 at 15:00):

for some time we thought of having two kind of (theories ...) field

Emilio Jesús Gallego Arias (May 27 2022 at 15:00):

in fact, that's how 2.0 should be

Emilio Jesús Gallego Arias (May 27 2022 at 15:00):

one theories field for legacy libs, and a newer one for the 2.0 model, which should be specified before we start to implement IMHO

Rudi Grinberg (May 27 2022 at 15:01):

Emilio Jesús Gallego Arias said:

Rudi Grinberg said:

Paolo Giarrusso said:

sorry, isn't there a bigger problem? opam cannot help with unsatisfied deps in (theories pkg1.A pkg2.A)...

yes, it can't help, but we want to design things so that it can help

I'm afraid that as two packages can provide the same lib/coq/user-contrib/A.v file, it is not possible to make this work well with the current lib model

Yup, but why do we care? Opam will already forbid installations like this. The goal here is to introduce a naming convention that allows us to associate names with packages. Not to solve the installation directory issues

Emilio Jesús Gallego Arias (May 27 2022 at 15:01):

but given that the only advantage is the opam hint, and most people don't even use opam

Emilio Jesús Gallego Arias (May 27 2022 at 15:01):

I'm not sure it is a priority

Emilio Jesús Gallego Arias (May 27 2022 at 15:01):

seems to me to make a mess in the current state

Emilio Jesús Gallego Arias (May 27 2022 at 15:01):

non-injective package names are a bad bad thing

Emilio Jesús Gallego Arias (May 27 2022 at 15:01):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

Rudi Grinberg said:

Paolo Giarrusso said:

sorry, isn't there a bigger problem? opam cannot help with unsatisfied deps in (theories pkg1.A pkg2.A)...

yes, it can't help, but we want to design things so that it can help

I'm afraid that as two packages can provide the same lib/coq/user-contrib/A.v file, it is not possible to make this work well with the current lib model

Yup, but why do we care? Opam will already forbid installations like this. The goal here is to introduce a naming convention that allows us to associate names with packages. Not to solve the installation directory issues

how you you do that when the mapping is not injective, Im at a loss

Rudi Grinberg (May 27 2022 at 15:04):

Let me try to understand the issue. Today, I can define theories that will install to the same location on the file system, right?

Emilio Jesús Gallego Arias (May 27 2022 at 15:05):

Yes, but the theory name is injective

Emilio Jesús Gallego Arias (May 27 2022 at 15:05):

wrt to the install place

Emilio Jesús Gallego Arias (May 27 2022 at 15:05):

so you can reason much easier

Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

if (name A) is already a theory, another one with the same name is an error

Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

the check needs to be strenghenen by the way due to sub-theories

Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

in the module namespace

Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

(recurse dirs)

Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

if you do (name pkg.A)

Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

ok, you do that, but you will throw pkg away anyways

Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

still the canonical name of the theory is A

Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

not pkg.A

Rudi Grinberg (May 27 2022 at 15:08):

Okay, but even if you throw it away, it still served its purpose.

Emilio Jesús Gallego Arias (May 27 2022 at 15:09):

it has served a purpose, however now users are extremely confused

Emilio Jesús Gallego Arias (May 27 2022 at 15:09):

as when they write (theories pkg.A)

Emilio Jesús Gallego Arias (May 27 2022 at 15:09):

that's unclear

Rudi Grinberg (May 27 2022 at 15:09):

and then in the 2.0 layout you alluded to, where x.A and y.A would co-exist, it would even become more useful

Emilio Jesús Gallego Arias (May 27 2022 at 15:09):

yes in the 2.0 layout it would much better

Emilio Jesús Gallego Arias (May 27 2022 at 15:09):

but now seems like a way to shoot ourselves in the foot

Emilio Jesús Gallego Arias (May 27 2022 at 15:10):

because what does (theories pkg1.A pkg2.A) mean?

Rudi Grinberg (May 27 2022 at 15:10):

Perhaps the . syntax is overloading notation here. What if it was pkg:A?

Emilio Jesús Gallego Arias (May 27 2022 at 15:10):

that's very confusing to users

Emilio Jesús Gallego Arias (May 27 2022 at 15:10):

even if it was pkg:A

Emilio Jesús Gallego Arias (May 27 2022 at 15:10):

what does the above mean?

Emilio Jesús Gallego Arias (May 27 2022 at 15:10):

that's a good point

Emilio Jesús Gallego Arias (May 27 2022 at 15:10):

the syntax, but even so it is confusing, and indeed, ambigous, so for sure that'd need a different syntax

Emilio Jesús Gallego Arias (May 27 2022 at 15:11):

in fact I had forgotten, but the reason I got rid of public_name was because it was not possible to determine

Rudi Grinberg (May 27 2022 at 15:11):

pkg:A means that A comes from pkg - nothing more. Qualifying which package public artifacts come from is a good thing.

Emilio Jesús Gallego Arias (May 27 2022 at 15:11):

if pkg.A meant module namespace pkg.A or package pkg module namespace A

Emilio Jesús Gallego Arias (May 27 2022 at 15:11):

Rudi Grinberg said:

pkg:A means that A comes from pkg - nothing more. Qualifying which package public artifacts comes from is a good thing.

it is a good thing, but for libraries using Coq Makefile

Emilio Jesús Gallego Arias (May 27 2022 at 15:12):

you have no idea, all you know is what it is in user contrib

Emilio Jesús Gallego Arias (May 27 2022 at 15:12):

so for example

Emilio Jesús Gallego Arias (May 27 2022 at 15:12):

module wasm.linear_register

Emilio Jesús Gallego Arias (May 27 2022 at 15:12):

could come from pkg compcert3 or from package compcert4

Rudi Grinberg (May 27 2022 at 15:12):

Yup, that's why I said there would be a fallback for coq makefile stuff to do the package-unqualified lookup.

Emilio Jesús Gallego Arias (May 27 2022 at 15:12):

as compcert is not using Dune

Emilio Jesús Gallego Arias (May 27 2022 at 15:13):

how do you know? All you can check is that the module lib/coq/user-contrib/wasm/linear_register.vo is there

Emilio Jesús Gallego Arias (May 27 2022 at 15:13):

so that's IMHO a very bad experience to users

Emilio Jesús Gallego Arias (May 27 2022 at 15:13):

as they may write compcert4:wasm.linear_register

Emilio Jesús Gallego Arias (May 27 2022 at 15:13):

and maybe the module is coming from pkg compcert3

Emilio Jesús Gallego Arias (May 27 2022 at 15:14):

and Dune has not means to warn them

Rudi Grinberg (May 27 2022 at 15:15):

perhaps then you're only allowed to write compcert4:wasm.linear_register if compcert4 is installed through dune?

Emilio Jesús Gallego Arias (May 27 2022 at 15:16):

that's what I meant above by using different fields, (legacy_theory ...) and (theory ...)

Emilio Jesús Gallego Arias (May 27 2022 at 15:16):

of using the : syntax we don't need that

Emilio Jesús Gallego Arias (May 27 2022 at 15:16):

so yes that'd be great, but I planned for 2.0 version

Rudi Grinberg (May 27 2022 at 15:17):

we use %{pkg:foo} elsewhere dune, but it's not very important

Emilio Jesús Gallego Arias (May 27 2022 at 15:17):

we could indeed do this for 1.0, at the cost of installing in both lib/coq/pkg and lib/coq/user-contrib, however I'm concerned about the size explosion, some Coq libs can reach the GiBs

Emilio Jesús Gallego Arias (May 27 2022 at 15:18):

For 2.0 I was planning to drop the constraint "non dunerized Coq libs can use dunerized Coq libs"

Emilio Jesús Gallego Arias (May 27 2022 at 15:18):

but we can do differently if we want

Rudi Grinberg (May 27 2022 at 15:19):

in dune, we kind of messed up the handling of binaries I feel. Nobody qualifies the package for the binaries they use and it makes it impossible to give good error messages and make sure people's dependencies are correct. I'd hate to see the same mistake repeated with coq.

Rudi Grinberg (May 27 2022 at 15:21):

Emilio Jesús Gallego Arias said:

we could indeed do this for 1.0, at the cost of installing in both lib/coq/pkg and lib/coq/user-contrib, however I'm concerned about the size explosion, some Coq libs can reach the GiBs

Yeah, that could indeed be an issue.

Emilio Jesús Gallego Arias (May 27 2022 at 15:22):

I agree we can do better with deps, however Dune doesn't really know about packaging

Emilio Jesús Gallego Arias (May 27 2022 at 15:22):

so that's not easy, unless we add some package manager capabilities

Emilio Jesús Gallego Arias (May 27 2022 at 15:22):

which would be cool

Rudi Grinberg (May 27 2022 at 15:22):

Indeed it would be cool and it's a goal of ours.

Emilio Jesús Gallego Arias (May 27 2022 at 15:23):

Coq "2.0" version of the language is a good chance to do things better, because I'm positive we can also modify Coq

Emilio Jesús Gallego Arias (May 27 2022 at 15:23):

much more easy than OCaml

Emilio Jesús Gallego Arias (May 27 2022 at 15:23):

our CI model is already tailored to quicker evolution as we don't promise a lot of stability w.r.t. APIs

Emilio Jesús Gallego Arias (May 27 2022 at 15:23):

(we can't sadly)

Emilio Jesús Gallego Arias (May 27 2022 at 15:27):

But in general all you propose seems great, the thing is how to so we have a reasonable transient state where we can port the large number of Coq libs

Rudi Grinberg (May 27 2022 at 15:37):

Alright let's composition going then so people can port.

Rudi Grinberg (May 28 2022 at 15:46):

@Karl Palmskog composition is done :scream:

Karl Palmskog (May 28 2022 at 15:46):

@Rudi Grinberg OK, how can I try out?

Karl Palmskog (May 28 2022 at 15:48):

I've several projects where I've been waiting for it

Rudi Grinberg (May 28 2022 at 15:50):

https://github.com/ocaml/dune/pull/5784

Karl Palmskog (May 28 2022 at 17:16):

I tried the PR branch on a project locally, whose packaging structure looks as follows (Dune is used in all packages):

coq-fourcolor  coq-graph-theory-general
        \     /                  \
   coq-graph-theory-planar       coq-graph-theory-ptt

Here, the base name is GraphTheory, and then the subpackages are GraphTheory.general, GraphTheory.ptt, ...

I then added dune like the following:

(coq.theory
 (name GraphTheory.ptt)
 (package coq-graph-theory-ptt)
 (theories GraphTheory.general)
...)

Everything then works fine with dune build. But when I build each opam package by pinning -k path, I get the following error, which I thought the PR would fix:

#=== ERROR while compiling coq-graph-theory-ptt.dev ===========================#
# context     2.1.2 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.13.0+options | pinned(file:///home/palmskog/src/coq/coq-community/graph-theory)
# path        ~/.opam/4.13.0+flambda+coq.dev/.opam-switch/build/coq-graph-theory-ptt.dev
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-graph-theory-ptt -j 15
# exit-code   1
# env-file    ~/.opam/log/coq-graph-theory-ptt-393868-7c2c75.env
# output-file ~/.opam/log/coq-graph-theory-ptt-393868-7c2c75.out
### output ###
# File "theories/ptt/dune", line 5, characters 11-30:
# 5 |  (theories GraphTheory.general)
#                ^^^^^^^^^^^^^^^^^^^
# Theory GraphTheory.general not found

Karl Palmskog (May 28 2022 at 17:18):

to me at least, the main benefit of "full composition" would be the possibility of using both dune build on CLI for multi-package projects, and use dune in opam packages...

Emilio Jesús Gallego Arias (May 28 2022 at 17:20):

@Karl Palmskog can you share the dune file for graphtheory

Karl Palmskog (May 28 2022 at 17:21):

you mean for coq-graph-theory-general?

Emilio Jesús Gallego Arias (May 28 2022 at 17:21):

ye

Emilio Jesús Gallego Arias (May 28 2022 at 17:21):

yes

Karl Palmskog (May 28 2022 at 17:21):

(coq.theory
 (name GraphTheory.general)
 (package coq-graph-theory-general)
 (synopsis "Graph theory definitions and results in Coq and MathComp")
 (flags :standard
   -w -notation-overridden
   -w -redundant-canonical-projection
   -w -projection-no-head-constant
   -w -duplicate-clear
   -w -elpi.add-const-for-axiom-or-sectionvar
   -w -ambiguous-paths))

Emilio Jesús Gallego Arias (May 28 2022 at 17:21):

what you wanna do worked fine in my branch

Emilio Jesús Gallego Arias (May 28 2022 at 17:21):

so yes it should work

Emilio Jesús Gallego Arias (May 28 2022 at 17:21):

I had a test for this effect, will push the test to Rudi / Ali branch

Karl Palmskog (May 28 2022 at 17:21):

I have the following:

dune                     3.2.0          pinned to version 3.2.0 at git+https://github.com/Alizter/dune#coq-compose

Emilio Jesús Gallego Arias (May 28 2022 at 17:22):

Yes it just seems the resolution code is not working inter-scope, that's an easy case

Karl Palmskog (May 28 2022 at 17:22):

I can push a branch with the exact Coq+Dune code if you want.

Emilio Jesús Gallego Arias (May 28 2022 at 17:23):

I don't need that, maybe Rudi / Ali want

Emilio Jesús Gallego Arias (May 28 2022 at 17:23):

seems like an obvious bug tho

Karl Palmskog (May 28 2022 at 17:24):

OK, then I leave up to @Rudi Grinberg if he wants more info

Rudi Grinberg (May 28 2022 at 17:27):

Could you make the workspace available somewhere?

Rudi Grinberg (May 28 2022 at 17:31):

Emilio Jesús Gallego Arias said:

what you wanna do worked fine in my branch

How did you resolve the name (theories GraphTheory.general) when building against installed packages? AFAIK, this isn't the subject of composition, but the subject of making theories work identically whether they're installed or local.

Rudi Grinberg (May 28 2022 at 17:32):

@Karl Palmskog your example isn't meant to work yet. When I saw composition, what I mean is assembling as many independent dune projects into the same workspace for development and having everything "just work". It doesn't mean reading external theories properly (that's a separate limitation)

Emilio Jesús Gallego Arias (May 28 2022 at 17:34):

Rudi Grinberg said:

Emilio Jesús Gallego Arias said:

what you wanna do worked fine in my branch

How did you resolve the name (theories GraphTheory.general) when building against installed packages? AFAIK, this isn't the subject of composition, but the subject of making theories work identically whether they're installed or local.

I need to reconstruct the installed layout from user-contrib + COQPATH

Emilio Jesús Gallego Arias (May 28 2022 at 17:35):

Rudi Grinberg said:

Karl Palmskog your example isn't meant to work yet. When I saw composition, what I mean is assembling as many independent dune projects into the same workspace for development and having everything "just work". It doesn't mean reading external theories properly (that's a separate limitation)

Umm, ah, so @Karl Palmskog 's example is with installed theory?

Emilio Jesús Gallego Arias (May 28 2022 at 17:35):

I thought it was in the same workspace, otherwise I'm not sure how it is different

Rudi Grinberg (May 28 2022 at 17:36):

@Emilio Jesús Gallego Arias After the boot discussion, I remembered another reason why we need public names in dune. We rely on them for lazy loading. So for example, when we resolve the name foo or foo.x, we know we need to look up foo/dune-package in the OCAMLPATH. I don't think that's relevent to coq yet, but it's something to keep in mind.

Emilio Jesús Gallego Arias (May 28 2022 at 17:36):

Yes, but we have that IANM as the public name is pkg.name

Rudi Grinberg (May 28 2022 at 17:37):

Emilio Jesús Gallego Arias said:

Rudi Grinberg said:

Karl Palmskog your example isn't meant to work yet. When I saw composition, what I mean is assembling as many independent dune projects into the same workspace for development and having everything "just work". It doesn't mean reading external theories properly (that's a separate limitation)

Umm, ah, so Karl Palmskog 's example is with installed theory?

Yes, in his example, he's pinning some of the packages and installing them through opam

Emilio Jesús Gallego Arias (May 28 2022 at 17:37):

you need indeed to resolve the equivalent of findlib-installed libraries lazily, but that's fine as it is a tree

Emilio Jesús Gallego Arias (May 28 2022 at 17:37):

Yes, I missed that

Karl Palmskog (May 28 2022 at 17:37):

yes, I'm using installed stuff through opam (by pinning). I thought this would be supported by full composition

Emilio Jesús Gallego Arias (May 28 2022 at 17:37):

Adding the installed stuff from opam is modular

Emilio Jesús Gallego Arias (May 28 2022 at 17:38):

so we can do a PR with workspace, inter-scope composition

Emilio Jesús Gallego Arias (May 28 2022 at 17:38):

and add a PR later on with support for installed_theories

Rudi Grinberg (May 28 2022 at 17:38):

That's a separate feature. If I understand how to do:

I need to reconstruct the installed layout from user-contrib + COQPATH

I should be able to implement it as well.

Emilio Jesús Gallego Arias (May 28 2022 at 17:38):

if that suits better the dev process

Emilio Jesús Gallego Arias (May 28 2022 at 17:38):

Rudi Grinberg said:

That's a separate feature. If I understand, how to do:

I need to reconstruct the installed layout from user-contrib + COQPATH

I should be able to implement it as well.

Yeah that's easy, modulo indeed the laziness, you don't want to scan user-contrib in full, but only under demand

Emilio Jesús Gallego Arias (May 28 2022 at 17:39):

That scanning can become a hot-spot in large Coq projects

Emilio Jesús Gallego Arias (May 28 2022 at 17:39):

But with Memo.t , 3.0 has good support for that

Rudi Grinberg (May 28 2022 at 17:39):

Can you give me a pointer in the docs with the spec for user-contrib + COQPATH?

Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

I need to go now sorry

Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

but I will give you later if noone steps for that

Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

user-contrib is basically $lib/coq/user-contrib

Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

and COQPATH is just a list of dirs, split by colons

Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

like OCAMLPATH

Rudi Grinberg (May 28 2022 at 17:40):

do you mean coq/user-contrib/$lib?

Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

and Coq merges all the dirs

Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

nope

Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

$lib/coq/user_contrib

Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

all the libs are dumped there :S

Karl Palmskog (May 28 2022 at 17:41):

here is the whole code, the last commit adds the theories stuff: https://github.com/coq-community/graph-theory/tree/split-wagner+dune-composition

This use case is not really fringe, it's how I expect most mature Coq projects to use Dune eventually

Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

$lib/coq/user-contrib/compcert/middle_end/bar.v

Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

for example

Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

Yes @Karl Palmskog it is not fringe, it is essential

Rudi Grinberg (May 28 2022 at 17:41):

but why do you put $lib? it's always lib/coq/user-contrib isn't it?

Emilio Jesús Gallego Arias (May 28 2022 at 17:42):

I mean, the basic use case

Emilio Jesús Gallego Arias (May 28 2022 at 17:42):

I mean $prefix/lib

Rudi Grinberg (May 28 2022 at 17:42):

for example, lib/coq/user-contrib/Ltac2 in my switch

Emilio Jesús Gallego Arias (May 28 2022 at 17:42):

except when you compose with Coq

Emilio Jesús Gallego Arias (May 28 2022 at 17:42):

sorry, I meant $lib for $prefix/lib, that was a bad choice

Emilio Jesús Gallego Arias (May 28 2022 at 17:43):

It's gonna be awecome when we have this

Emilio Jesús Gallego Arias (May 28 2022 at 17:43):

then we can pretty much bump (using coq $version)

Rudi Grinberg (May 28 2022 at 17:43):

ok. so we can assume that $prefix/lib/coq/user-contrib/%{lib} corresponds to a single library?

Emilio Jesús Gallego Arias (May 28 2022 at 17:43):

and start improving all that we discussed

Emilio Jesús Gallego Arias (May 28 2022 at 17:43):

@Rudi Grinberg yes a theory A.B.C is mapped to A/B/C.v

Emilio Jesús Gallego Arias (May 28 2022 at 17:44):

à la Haskell

Karl Palmskog (May 28 2022 at 17:44):

user-contrib/%{lib} can be used by several libraries (which have their own subdirectory under %{lib})

Emilio Jesús Gallego Arias (May 28 2022 at 17:44):

need to really go now, I'm so excited that's gonna be so cool

Rudi Grinberg (May 28 2022 at 17:44):

Ttyl. Perhaps Karl will help me understand meanwhile

Karl Palmskog (May 28 2022 at 17:45):

I will do my best, but I don't understand too much about Dune internals.

Rudi Grinberg (May 28 2022 at 17:45):

You don't need to know anything about that. So given a theory A/B/C.v, do you expect users to write (theories a.b.c) to use it, right?

Karl Palmskog (May 28 2022 at 17:46):

since C.v is a file, I would expect to write (theories a.b)

Emilio Jesús Gallego Arias (May 28 2022 at 17:46):

They can also write (theories a) to get a.* in scope

Emilio Jesús Gallego Arias (May 28 2022 at 17:46):

yes, in this case only a and a.b are possible

Emilio Jesús Gallego Arias (May 28 2022 at 17:47):

there is quite a bit of overlapping actually, there are some invariants that are not enforced by Coq actually

Rudi Grinberg (May 28 2022 at 17:47):

okay, but this is weird, isn't it? one can define the following in dune:

(coq.theory (name a.b))
(coq.theory (name a.c))

but then use the shared prefix a as in (coq.theory .. (theories a))?

Emilio Jesús Gallego Arias (May 28 2022 at 17:47):

yes, that's a common use case

Emilio Jesús Gallego Arias (May 28 2022 at 17:47):

it works that way

Emilio Jesús Gallego Arias (May 28 2022 at 17:47):

so individiaul packages can contribute to a "namespace"

Emilio Jesús Gallego Arias (May 28 2022 at 17:48):

like math-comp

Emilio Jesús Gallego Arias (May 28 2022 at 17:48):

that's powerful but not fully specified, another point to work for 2.0 version of the build language

Rudi Grinberg (May 28 2022 at 17:49):

It may be "powerful", but it's also completely opaque to package managers (as I've pointed out earlier).

Karl Palmskog (May 28 2022 at 17:49):

in the Coq ecosystem, we try to enforce that two packages do not write to the exact same directory in user-contrib, but there is no guarantee. It's pretty common though that packages write to a subdirectory defined by another package (e.g., there is the base mathcomp directory, then mathcomp-finmap package writes .vo files into mathcomp/finmap to get mathcomp.finmap name)

Rudi Grinberg (May 28 2022 at 17:50):

Rudi Grinberg said:

okay, but this is weird, isn't it? one can define the following in dune:

(coq.theory (name a.b))
(coq.theory (name a.c))

but then use the shared prefix a as in (coq.theory .. (theories a))?

@Karl Palmskog what do you think about this? do you expect this to work? I don't think this works today with dune

Emilio Jesús Gallego Arias (May 28 2022 at 17:50):

Yes it is opaque, needs to be improved. But it is also common, think how haskell manages for example the Data.* namespace

Rudi Grinberg (May 28 2022 at 17:51):

Emilio Jesús Gallego Arias said:

Yes it is opaque, needs to be improved. But it is also common, think how haskell manages for example the Data.* namespace

In Haskell, one writes the names of cabal packages in the cabal files, not the names of raw namespaces

Emilio Jesús Gallego Arias (May 28 2022 at 17:51):

Yes it doesn't work today, but I'm aware of the issue, not sure what to do tho, there are several issues

Karl Palmskog (May 28 2022 at 17:51):

in my view, a single directory where you put .v files should have a single coq.theory name declaration

Emilio Jesús Gallego Arias (May 28 2022 at 17:51):

so I was expecting to finish inter-scope composition, then grab what users are doing

Emilio Jesús Gallego Arias (May 28 2022 at 17:51):

are doing, real use cases

Karl Palmskog (May 28 2022 at 17:52):

so I would not expect for it to be allowed to have a dune file which says: (coq.theory (name a.b)) (coq.theory (name a.c)).

Emilio Jesús Gallego Arias (May 28 2022 at 17:53):

@Karl Palmskog that's bizarre, that's basically how math-comp dune works

Emilio Jesús Gallego Arias (May 28 2022 at 17:53):

For now I think we can go ahead

Emilio Jesús Gallego Arias (May 28 2022 at 17:53):

with the current "strict" name treatment

Emilio Jesús Gallego Arias (May 28 2022 at 17:53):

until we can drop compat from Dune to non-dune, and use real packages

Karl Palmskog (May 28 2022 at 17:54):

don't you put multiple dune files in subdirectories in mathcomp itself?

Rudi Grinberg (May 28 2022 at 17:54):

Karl Palmskog said:

so I would not expect for it to be allowed to have a dune file which says: (coq.theory (name a.b)) (coq.theory (name a.c)).

Okay, well what about this:

$ ls -R
A/ A/B A/C
$ cat A/B/dune
(coq.theory (name A.B))
$ cat A/C/dune
(coq.theory (name A.C))

And then you can use (theories A) elsewhere?

Emilio Jesús Gallego Arias (May 28 2022 at 17:54):

Indeed @Rudi Grinberg you make a good point, about that stuff being specific to Cabal, if you don't use cabal you are in a different scenario

Emilio Jesús Gallego Arias (May 28 2022 at 17:54):

here we can (yet) switch everthing

Karl Palmskog (May 28 2022 at 17:54):

@Rudi Grinberg yes, I would expect that to work

Emilio Jesús Gallego Arias (May 28 2022 at 17:55):

That's fine, see https://github.com/math-comp/math-comp/pull/316

Emilio Jesús Gallego Arias (May 28 2022 at 17:55):

but then use the shared prefix a as in (coq.theory .. (theories a))?

My guess is that we don't need to support that, but we need to port more developments to Dune

Karl Palmskog (May 28 2022 at 17:56):

right, yes, the MathComp PR declares one coq.theory per subdirectory. I was only saying a single dune file with multiple coq.theory would be an anomaly

Emilio Jesús Gallego Arias (May 28 2022 at 17:57):

A single dune file with several coq.theory is also fine

Rudi Grinberg (May 28 2022 at 17:57):

I guess I just don't see it as a sane feature at all. For example, someone might create some random theory (name a.b.c.d) and now everyone that specified (theories a) should be recompiled?!

Emilio Jesús Gallego Arias (May 28 2022 at 17:57):

tho not in all cases

Emilio Jesús Gallego Arias (May 28 2022 at 17:57):

Rudi Grinberg said:

I guess I just don't see it as a sane feature at all. For example, someone might create some random theory (a.b.c.d) and now everyone that specified (theories a) should be recompiled?!

yes, as I say let's not support that for now

Emilio Jesús Gallego Arias (May 28 2022 at 17:57):

But indeed, we can't anticipate how people has structured thing

Emilio Jesús Gallego Arias (May 28 2022 at 17:57):

things

Rudi Grinberg (May 28 2022 at 18:04):

Back to making this work somehow, if we have a user-contrib as follows:

a/foo.v a/b/bar.v

do we let the users write a and a.b?

Rudi Grinberg (May 28 2022 at 18:05):

Since we have no idea if this came from a single theory a or separate theories a and a.b?

Karl Palmskog (May 28 2022 at 18:07):

currently, it's allowed to write a and a.b even if they (a/... and a/b/...) exist. But as per above, we try to avoid having packages that do this

Rudi Grinberg (May 28 2022 at 18:08):

didn't Emilio just say that mathcomp does this?

Karl Palmskog (May 28 2022 at 18:09):

my view is that mathcomp writes disjoint subdirectories incrementally. It first creates mathcomp/ssreflect, then mathcomp/algebra, etc.

Rudi Grinberg (May 28 2022 at 18:10):

okay, but how should dune know that mathcomp itself isn't a valid theory?

Rudi Grinberg (May 28 2022 at 18:10):

by the absence of a mathcomp/*.v?

Karl Palmskog (May 28 2022 at 18:10):

does it need to know that? if so, I'd go with absence of mathcomp/*.v, yes

Karl Palmskog (May 28 2022 at 18:13):

but I think Emilio wanted (theories mathcomp) to work, even though there's no mathcomp/*.v. This theories declaration says you just depend on "whatever" happens to be in mathcomp, recursively. I think this is sloppy, and I wouldn't do it, but fine by me if it's supported.

Rudi Grinberg (May 28 2022 at 18:13):

IMO, the only kind of names that belong inside (theories ..) are those that were defined with (name ..) somewhere.

Karl Palmskog (May 28 2022 at 18:13):

this would be enough for me to get all my work done

Karl Palmskog (May 28 2022 at 18:14):

but I can see Emilio's argument (I think) that it's more flexible to be laxer than that.

Rudi Grinberg (May 28 2022 at 18:14):

I also find it amusing that you think that including stdlib in the theories field explicitly will impose on beginners, but this namespacing scheme will not :)

Rudi Grinberg (May 28 2022 at 18:15):

Karl Palmskog said:

but I can see Emilio's argument (I think) that it's more flexible to be laxer than that.

I think Emilio is reconsidering:

yes, as I say let's not support that for now

Karl Palmskog (May 28 2022 at 18:16):

well, beginners will generally know the name of the third-party libraries they will use. They will use some boilerplate (theories ...) for this given by someone else. But then they care about that particular library, and stdlib is something in the background that most people assume is there

Rudi Grinberg (May 28 2022 at 18:25):

Karl Palmskog said:

does it need to know that? if so, I'd go with absence of mathcomp/*.v, yes

Yes, it needs to know. Otherwise we're introducing differences between installed and local theories. For example, I might have (coq.theory (name mathcomp.foo)) locally, I can only use mathcomp.foo, but now that it's installed, it's suddenly available as mathcomp as well.

Rudi Grinberg (May 28 2022 at 18:26):

I suppose we could relax the meaning of the (theories ..) field locally as well, but I don't think that's a good idea

Rudi Grinberg (May 28 2022 at 19:13):

@Karl Palmskog how should dune know where the user-contrib folder should come from?

Karl Palmskog (May 28 2022 at 19:14):

I mean, I always assume it's known by the coqc executable

Karl Palmskog (May 28 2022 at 19:14):

wasn't there work to query coqc for this?

Rudi Grinberg (May 28 2022 at 19:16):

It's known by the coq executable, but dune needs to know as well to add the appropriate dependencies.

Rudi Grinberg (May 28 2022 at 19:18):

I suppose there's coqc -config, but it's kind of problematic to use it. Because now it means that we need a different code path when composing workspaces with coq itself.

Karl Palmskog (May 28 2022 at 19:18):

I think I have used coqc -where for some other tool

Karl Palmskog (May 28 2022 at 19:19):

basically, it's assumed to be at:

echo `coqc -where`/user-contrib

Karl Palmskog (May 28 2022 at 19:20):

but I have no idea if that's the recommended way to obtain the path

Rudi Grinberg (May 28 2022 at 19:20):

what happens when coqc is part of the dune workspace?

Karl Palmskog (May 28 2022 at 19:20):

no idea unfortunately, I always use Coq installed by opam or some other package manager like Nix

Karl Palmskog (May 28 2022 at 19:21):

but I think very few Coq users will have Coq as part of their Dune workspace. Essentially only useful for Coq devs and plugin devs

Rudi Grinberg (May 28 2022 at 19:21):

In OCaml, we have opam setting OCAMLPATH for us

Rudi Grinberg (May 28 2022 at 19:22):

I'll just hard code it to ~/.opam/$switch/coq/lib/user-contrib for now. Otherwise, users can set COQLIB.

Karl Palmskog (May 28 2022 at 19:23):

oof, I think that will break Nix

Rudi Grinberg (May 28 2022 at 19:23):

Why would it?

Karl Palmskog (May 28 2022 at 19:23):

or maybe they actually set COQLIB

Karl Palmskog (May 28 2022 at 19:25):

Nix handles user-contrib some peculiar way I think

Rudi Grinberg (May 28 2022 at 19:25):

Actually, it's COQPATH?

Rudi Grinberg (May 28 2022 at 19:25):

Karl Palmskog said:

Nix handles user-contrib some peculiar way I think

who do we ask about it?

Karl Palmskog (May 28 2022 at 19:27):

maybe you can just go with what you proposed and Emilio can ping in some Nix expert and see if it affects them

Karl Palmskog (May 28 2022 at 19:28):

I think coq_makefile might be a guide to what the variables are usually called. For example:

COQLIB            := $(COQMF_COQLIB)

and then COQMF_COQLIB is defined by coq_makefile during Makefile generation:

COQMF_COQLIB=~/.opam/$switch/lib/coq/

Karl Palmskog (May 28 2022 at 19:29):

so I guess you could look at coq_makefile for how it's "supposed" to be done.

Karl Palmskog (May 28 2022 at 19:30):

the assumption is that people might want to redefine COQLIB to something by setting env vars

Rudi Grinberg (May 28 2022 at 19:30):

Is COQPATH documented somewhere?

Karl Palmskog (May 28 2022 at 19:31):

I don't see any COQPATH in stuff generated by coq_makefile

Ali Caglayan (May 28 2022 at 19:34):

Rudi Grinberg said:

I'll just hard code it to ~/.opam/$switch/coq/lib/user-contrib for now. Otherwise, users can set COQLIB.

Beware COQLIB is one directory up so it would be $COQLIB/user-contrib.

Ali Caglayan (May 28 2022 at 19:34):

I don't know about any COQPATH, only COQLIB

Ali Caglayan (May 28 2022 at 19:35):

At least internally, coqc is looking for packages in COQLIB if it exists.

Rudi Grinberg (May 28 2022 at 19:36):

So suppose I set COQLIB=foo, coq should look up packages in foo/ or foo/user-contrib?

Karl Palmskog (May 28 2022 at 19:37):

foo/user-contrib, as far as I know

Ali Caglayan (May 28 2022 at 19:38):

And furthermore, stdlib in foo/theories.

Ali Caglayan (May 28 2022 at 19:40):

Here is coq's internal doc on that: https://github.com/coq/coq/blob/master/boot/env.mli

Paolo Giarrusso (May 28 2022 at 20:49):

Karl Palmskog said:

this would be enough for me to get all my work done

(looks at the context) is it actually the case that packages use disjoint logical paths in -Q options? you can't always split libraries to fix that (as you suggest) — you can only split foo into foo.a and foo.b if there's no mutual dependency between them (e.g. foo.a uses foo.b or viceversa)

Paolo Giarrusso (May 28 2022 at 20:50):

at least, I don't see how to specify mutual dependencies in the dune source language, while with coq_makefile it is trivial (just specify multiple -Q options in one _CoqProject)

Paolo Giarrusso (May 28 2022 at 20:51):

and I'd be happy to be wrong, since this is one thing ~I'll have to sort out~ at work (on our side) to complete our dune migration (okay wasn't _that_ hard)

Karl Palmskog (May 28 2022 at 20:59):

is it actually the case that packages use disjoint logical paths in -Q options?

probably not, but I was talking about the projects I would conceivably use Dune for. Non-disjoint paths would be bad practice and thus not part of my projects...

Paolo Giarrusso (May 28 2022 at 21:04):

ah, I thought you were wearing your coq-community hat

Karl Palmskog (May 28 2022 at 21:25):

people who want some strange -Q/-R options will still have coq_makefile, etc. But in the coq-community GitHub org, for example, we will make sure to use best practices for building, including disjoint -Q. So if Dune even goes so far as mandating that, that's fine by me...

Emilio Jesús Gallego Arias (May 29 2022 at 12:25):

Indeed I think that (theories mathcomp) should not work, even if it will work for a while "by accident"

Emilio Jesús Gallego Arias (May 29 2022 at 12:26):

What happens when a theory with boot is in scope is a good question

Emilio Jesús Gallego Arias (May 29 2022 at 12:26):

I guess in this case installed_theories should be empty

Emilio Jesús Gallego Arias (May 29 2022 at 12:27):

so no lookup

Emilio Jesús Gallego Arias (May 29 2022 at 12:27):

We don't really need -open I think, we already have -R, maybe we should enforce it is only used in the current compilation unit

Ali Caglayan (May 29 2022 at 12:32):

@Emilio Jesús Gallego Arias "-open" has much more sane semantics than "-R" IMO

Ali Caglayan (May 29 2022 at 12:33):

It is already massively confusing for users (and me) to have -R and -Q around.

Ali Caglayan (May 29 2022 at 12:34):

At least with "-open" (not particularly happy with the name but oh well) it is obvious that the loadpath is not being modified.

Ali Caglayan (May 29 2022 at 12:35):

-Q has a simple modification to the loadpath

Ali Caglayan (May 29 2022 at 12:35):

-R can do whatever and that is really tricky to treat in tooling

Ali Caglayan (May 29 2022 at 12:36):

Here is something that happens today: -R and -Q can be interleaved many times, and their order between each other matters.

Ali Caglayan (May 29 2022 at 12:40):

-R exists as a convenience to users. We should support a proper convenience "-open" and stop using -R in tooling all together.

Rudi Grinberg (May 29 2022 at 16:16):

Emilio Jesús Gallego Arias said:

I guess in this case installed_theories should be empty

What's the installed_theories field is about?

Emilio Jesús Gallego Arias (May 30 2022 at 12:23):

@Ali Caglayan yes, the first we should do is to restrict -R to a single invocation, and enforce the invariant that the file passed to coqc is actually scoped by -R

Emilio Jesús Gallego Arias (May 30 2022 at 12:23):

I just meant we can reuse the option

Ali Caglayan (May 30 2022 at 12:25):

Still the non-commutativity of -R and -Q remains.

Ali Caglayan (May 30 2022 at 12:28):

I suggest restricting -R as you say, or even go as far as deprecating it.

Ali Caglayan (May 30 2022 at 12:28):

The alternative should be a properly implemented -open

Ali Caglayan (May 30 2022 at 12:29):

Here we have a choice, do we want to be able to -open multiple theories?

Ali Caglayan (May 30 2022 at 12:29):

I think that would not be a good idea

Emilio Jesús Gallego Arias (May 30 2022 at 12:29):

In what sense?

Emilio Jesús Gallego Arias (May 30 2022 at 12:29):

In what sense does the non-communitativy remain? You mean after fixing it, or before

Ali Caglayan (May 30 2022 at 12:29):

For instance today, the Coq stdlib and typically the current development are "-open"ed.

Emilio Jesús Gallego Arias (May 30 2022 at 12:29):

Yes, the first needs to be fixed

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

-R really means -open, I find -open confusing as this is not OCaml where you do open Foo

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

Coq actually has better semantics than OCaml

Ali Caglayan (May 30 2022 at 12:30):

You can have -Q A/B Foo and -R A Bar which changes the semantic

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

Keeping -R is OK as for a lot of users it will keep working

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

@Ali Caglayan that should error

Emilio Jesús Gallego Arias (May 30 2022 at 12:31):

Another very unfortunate thing -R does today is to flatten the namespace beyond open

Emilio Jesús Gallego Arias (May 30 2022 at 12:31):

that should be fixed

Ali Caglayan (May 30 2022 at 12:31):

No error, only a warning.

Emilio Jesús Gallego Arias (May 30 2022 at 12:32):

Stdlib is prime offender, but adding From Coq would alleviate it, as in this case the wildcard is explicit

Ali Caglayan (May 30 2022 at 12:32):

Not in the stdlib tho

Ali Caglayan (May 30 2022 at 12:32):

We shouldn't have to use From Coq in the stdlib

Emilio Jesús Gallego Arias (May 30 2022 at 12:32):

Ali Caglayan said:

No error, only a warning.

I don't see that as a sane semantics, IMHO it should eventually error, again it breaks injectivity which is very bad (means you can't maintain proper reverse maps for example)

Emilio Jesús Gallego Arias (May 30 2022 at 12:32):

I mean stdlib users

Ali Caglayan (May 30 2022 at 12:33):

Emilio Jesús Gallego Arias said:

Ali Caglayan said:

No error, only a warning.

I don't see that as a sane semantics, IMHO it should eventually error, again it breaks injectivity which is very bad (means you can't maintain proper reverse maps for example)

I'm not suggesting that, that is what happens today.

Emilio Jesús Gallego Arias (May 30 2022 at 12:33):

they can write Require List where they mean Require Lists.List etc...

Emilio Jesús Gallego Arias (May 30 2022 at 12:33):

Yes what happens today is not good at all

Emilio Jesús Gallego Arias (May 30 2022 at 12:33):

it is a mess

Emilio Jesús Gallego Arias (May 30 2022 at 12:33):

I don't think anyone disagrees on the current state needing work

Ali Caglayan (May 30 2022 at 12:34):

Here is a proposal for the semantics of -open or whatever we want to call it:

• If I see a Require Import in a file, I should decorate it to From ... Require Import. The From to use is whatever was passed to -open.

Ali Caglayan (May 30 2022 at 12:35):

We should have all Require Import's use From internally

Ali Caglayan (May 30 2022 at 12:36):

Keeping the name -R for such an option is dumb IMO, since it means "Recursive" and it is not even that anymore.

Paolo Giarrusso (May 30 2022 at 12:38):

what if I use Require with a full path?

Paolo Giarrusso (May 30 2022 at 12:39):

and I guess you're assuming a single -open

Emilio Jesús Gallego Arias (May 30 2022 at 12:51):

That semantics seem too weak to me

Emilio Jesús Gallego Arias (May 30 2022 at 12:51):

It may be dumb, but if that keeps compat with a lot of 3rd party developments, that's dumb but a great time saver

Emilio Jesús Gallego Arias (May 30 2022 at 12:52):

-open is again not a very good name, as we don't "open" things in Coq

Karl Palmskog (May 30 2022 at 12:54):

hmm, isn't "Import" quite close to the SML "open"? [Semantically]

Emilio Jesús Gallego Arias (May 30 2022 at 12:56):

I don't know, I would be surprised if it were

Emilio Jesús Gallego Arias (May 30 2022 at 12:56):

at least, implementation wise

Emilio Jesús Gallego Arias (May 30 2022 at 12:56):

anyways my point is that it is not opem

Emilio Jesús Gallego Arias (May 30 2022 at 12:56):

indeed, -open means something more like "import"

Emilio Jesús Gallego Arias (Jun 02 2022 at 09:28):

By the way @Rudi Grinberg , turns out that jsCoq for example does already maintain a map from Coq modules to the corresponding package that is implemented it. This is used for lazy downloading of theories, but indeed, that could be useful for Dune too.

The main problem is that it is a kind of global database, in the sense that it is hard for Dune to know that (theories bar) maps to some package. If the user already knows to write (theories pkg:bar) indeed they have already done the hard part of the work themselves, which to resolve the module to the package, haven't they?

Rudi Grinberg (Jun 02 2022 at 15:07):

Yes, that's exactly it. I don't think it's a very big burden either

Last updated: Jun 03 2023 at 15:31 UTC