Stream: Dune devs & users

Topic: Public/Private names?


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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:43):

For Coq, that would be the only use

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:43):

you have the package tho

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:44):

but yeah that doesn't help a lot

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:44):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:44):

That would rule out all of the current Coq developments

view this post on Zulip Rudi Grinberg (May 27 2022 at 14:44):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:44):

IIUC

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:45):

then we hope to do a 2.0 which is more principled

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:45):

do you have an example?

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:46):

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

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

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

view this post on Zulip Rudi Grinberg (May 27 2022 at 14:47):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:47):

1.0 has to work with non-dunerized libs

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:48):

I think 2.0 requires both more metadata and changes in Coq

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:49):

1

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:51):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:54):

what does 2 do that 3 doesn't?

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:54):

we already do that

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:54):

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:55):

as it is in conflict with pkg1

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

view this post on Zulip Rudi Grinberg (May 27 2022 at 14:56):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:57):

but you still can solve it using -I

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:57):

in Coq, once you are there, you are boom

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:57):

as both map to the same filesystem location

view this post on Zulip Paolo Giarrusso (May 27 2022 at 14:57):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:57):

I'm talking about the present

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:58):

not in lib/coq/user-contrib

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:59):

Yes, that's the goal

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:00):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:00):

in fact, that's how 2.0 should be

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:01):

I'm not sure it is a priority

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:01):

seems to me to make a mess in the current state

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:01):

non-injective package names are a bad bad thing

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:05):

Yes, but the theory name is injective

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:05):

wrt to the install place

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:05):

so you can reason much easier

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

in the module namespace

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

(recurse dirs)

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

if you do (name pkg.A)

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

still the canonical name of the theory is A

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:06):

not pkg.A

view this post on Zulip Rudi Grinberg (May 27 2022 at 15:08):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:09):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:09):

as when they write (theories pkg.A)

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:09):

that's unclear

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:09):

yes in the 2.0 layout it would much better

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:09):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:10):

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

view this post on Zulip Rudi Grinberg (May 27 2022 at 15:10):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:10):

that's very confusing to users

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:10):

even if it was pkg:A

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:10):

what does the above mean?

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:10):

that's a good point

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

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

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

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

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

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

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

so for example

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

module wasm.linear_register

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

could come from pkg compcert3 or from package compcert4

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

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

as compcert is not using Dune

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:13):

so that's IMHO a very bad experience to users

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:13):

as they may write compcert4:wasm.linear_register

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:13):

and maybe the module is coming from pkg compcert3

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

and Dune has not means to warn them

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:16):

of using the : syntax we don't need that

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:16):

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

view this post on Zulip Rudi Grinberg (May 27 2022 at 15:17):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:18):

but we can do differently if we want

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

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

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

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

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

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

which would be cool

view this post on Zulip Rudi Grinberg (May 27 2022 at 15:22):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:23):

much more easy than OCaml

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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 15:23):

(we can't sadly)

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

view this post on Zulip Rudi Grinberg (May 27 2022 at 15:37):

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:46):

@Karl Palmskog composition is done :scream:

view this post on Zulip Karl Palmskog (May 28 2022 at 15:46):

@Rudi Grinberg OK, how can I try out?

view this post on Zulip Karl Palmskog (May 28 2022 at 15:48):

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:50):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:20):

@Karl Palmskog can you share the dune file for graphtheory

view this post on Zulip Karl Palmskog (May 28 2022 at 17:21):

you mean for coq-graph-theory-general?

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:21):

ye

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:21):

yes

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:21):

what you wanna do worked fine in my branch

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:21):

so yes it should work

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

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

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

view this post on Zulip Karl Palmskog (May 28 2022 at 17:22):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:23):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:23):

seems like an obvious bug tho

view this post on Zulip Karl Palmskog (May 28 2022 at 17:24):

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 17:27):

Could you make the workspace available somewhere?

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:36):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:37):

Yes, I missed that

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:37):

Adding the installed stuff from opam is modular

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:38):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:38):

and add a PR later on with support for installed_theories

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:38):

if that suits better the dev process

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:39):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:39):

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 17:39):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

I need to go now sorry

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

but I will give you later if noone steps for that

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

like OCAMLPATH

view this post on Zulip Rudi Grinberg (May 28 2022 at 17:40):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:40):

and Coq merges all the dirs

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

nope

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

$lib/coq/user_contrib

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

all the libs are dumped there :S

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

for example

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:41):

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 17:41):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:42):

I mean, the basic use case

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:42):

I mean $prefix/lib

view this post on Zulip Rudi Grinberg (May 28 2022 at 17:42):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:42):

except when you compose with Coq

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:42):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:43):

It's gonna be awecome when we have this

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:43):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:43):

and start improving all that we discussed

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:44):

à la Haskell

view this post on Zulip Karl Palmskog (May 28 2022 at 17:44):

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

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 17:44):

Ttyl. Perhaps Karl will help me understand meanwhile

view this post on Zulip Karl Palmskog (May 28 2022 at 17:45):

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

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

view this post on Zulip Karl Palmskog (May 28 2022 at 17:46):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:46):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:46):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:47):

yes, that's a common use case

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:47):

it works that way

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:47):

so individiaul packages can contribute to a "namespace"

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:48):

like math-comp

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

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

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

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:51):

are doing, real use cases

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:53):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:53):

For now I think we can go ahead

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:53):

with the current "strict" name treatment

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

view this post on Zulip Karl Palmskog (May 28 2022 at 17:54):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:54):

here we can (yet) switch everthing

view this post on Zulip Karl Palmskog (May 28 2022 at 17:54):

@Rudi Grinberg yes, I would expect that to work

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:55):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:57):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:57):

tho not in all cases

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:57):

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

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:57):

things

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

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

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 18:08):

didn't Emilio just say that mathcomp does this?

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 18:10):

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 18:10):

by the absence of a mathcomp/*.v?

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

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

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

view this post on Zulip Karl Palmskog (May 28 2022 at 18:13):

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

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

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

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

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

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

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 19:13):

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

view this post on Zulip Karl Palmskog (May 28 2022 at 19:14):

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

view this post on Zulip Karl Palmskog (May 28 2022 at 19:14):

wasn't there work to query coqc for this?

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

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

view this post on Zulip Karl Palmskog (May 28 2022 at 19:18):

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

view this post on Zulip Karl Palmskog (May 28 2022 at 19:19):

basically, it's assumed to be at:

echo `coqc -where`/user-contrib

view this post on Zulip Karl Palmskog (May 28 2022 at 19:20):

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 19:20):

what happens when coqc is part of the dune workspace?

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

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 19:21):

In OCaml, we have opam setting OCAMLPATH for us

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

view this post on Zulip Karl Palmskog (May 28 2022 at 19:23):

oof, I think that will break Nix

view this post on Zulip Rudi Grinberg (May 28 2022 at 19:23):

Why would it?

view this post on Zulip Karl Palmskog (May 28 2022 at 19:23):

or maybe they actually set COQLIB

view this post on Zulip Karl Palmskog (May 28 2022 at 19:25):

Nix handles user-contrib some peculiar way I think

view this post on Zulip Rudi Grinberg (May 28 2022 at 19:25):

Actually, it's COQPATH?

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

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

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

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

view this post on Zulip Karl Palmskog (May 28 2022 at 19:30):

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

view this post on Zulip Rudi Grinberg (May 28 2022 at 19:30):

Is COQPATH documented somewhere?

view this post on Zulip Karl Palmskog (May 28 2022 at 19:31):

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

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

view this post on Zulip Ali Caglayan (May 28 2022 at 19:34):

I don't know about any COQPATH, only COQLIB

view this post on Zulip Ali Caglayan (May 28 2022 at 19:35):

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

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

view this post on Zulip Karl Palmskog (May 28 2022 at 19:37):

foo/user-contrib, as far as I know

view this post on Zulip Ali Caglayan (May 28 2022 at 19:38):

And furthermore, stdlib in foo/theories.

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (May 28 2022 at 21:04):

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2022 at 12:26):

I guess in this case installed_theories should be empty

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2022 at 12:27):

so no lookup

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

view this post on Zulip Ali Caglayan (May 29 2022 at 12:32):

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

view this post on Zulip Ali Caglayan (May 29 2022 at 12:33):

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

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

view this post on Zulip Ali Caglayan (May 29 2022 at 12:35):

-Q has a simple modification to the loadpath

view this post on Zulip Ali Caglayan (May 29 2022 at 12:35):

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

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

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

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

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

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

I just meant we can reuse the option

view this post on Zulip Ali Caglayan (May 30 2022 at 12:25):

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

view this post on Zulip Ali Caglayan (May 30 2022 at 12:28):

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

view this post on Zulip Ali Caglayan (May 30 2022 at 12:28):

The alternative should be a properly implemented -open

view this post on Zulip Ali Caglayan (May 30 2022 at 12:29):

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

view this post on Zulip Ali Caglayan (May 30 2022 at 12:29):

I think that would not be a good idea

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

In what sense?

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

view this post on Zulip Ali Caglayan (May 30 2022 at 12:29):

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

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

Yes, the first needs to be fixed

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

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

Coq actually has better semantics than OCaml

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

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

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

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

@Ali Caglayan that should error

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

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

that should be fixed

view this post on Zulip Ali Caglayan (May 30 2022 at 12:31):

No error, only a warning.

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

view this post on Zulip Ali Caglayan (May 30 2022 at 12:32):

Not in the stdlib tho

view this post on Zulip Ali Caglayan (May 30 2022 at 12:32):

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

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

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

I mean stdlib users

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

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

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

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

Yes what happens today is not good at all

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

it is a mess

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

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

view this post on Zulip Ali Caglayan (May 30 2022 at 12:34):

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

view this post on Zulip Ali Caglayan (May 30 2022 at 12:35):

We should have all Require Import's use From internally

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

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:38):

what if I use Require with a full path?

view this post on Zulip Paolo Giarrusso (May 30 2022 at 12:39):

and I guess you're assuming a single -open

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

That semantics seem too weak to me

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

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

view this post on Zulip Karl Palmskog (May 30 2022 at 12:54):

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

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

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

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

at least, implementation wise

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

anyways my point is that it is not opem

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

indeed, -open means something more like "import"

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

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