Stream: Dune devs & users

Topic: Composition of installed theories


view this post on Zulip Ali Caglayan (Feb 11 2023 at 21:08):

Following https://github.com/ocaml/dune/issues/6982 I've implemented some initial support for composition of installed theories https://github.com/ocaml/dune/pull/7047. Please try it out and report any thing that doesn't work.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 16:18):

Hi folks, this PR is almost ready, modulo some minor improvements and more tests.

That being the main blocker for 1.0 language release, we will start deprecating older coq lang versions

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 16:19):

In particular there is a big incompatiblity between dune lang 0.8 and earlier versions.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 16:19):

Earlier versions added by default all of user-contrib, but newer versions don't.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 16:19):

So you need to explicitly add your library

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 16:20):

To me, the main question for the 1.0 Coq dune lang is whether we should keep the implicit stdlib behavior enabled, or on the contrary, require users to declare Coq in their list of theories.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 16:21):

I think I'd like a roadmap as follows:

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 18:41):

Actually Karl's comment on a different thread made me think that we should try to see if making include_subdirs qualified the default for 1.0

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 19:06):

Include_subdirs qualified seems reasonable for 0.8?

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 19:07):

Stdlib with -Q seems good but much more invasive

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:14):

Paolo Giarrusso said:

Include_subdirs qualified seems reasonable for 0.8?

I'd depend if that's easy to implement

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:15):

Paolo Giarrusso said:

Stdlib with -Q seems good but much more invasive

That can be an option, however we gotta start at some point IMHO.

But indeed there is a tension on how to push users to migrate to saner setups. But it is easy to keep -R for the stdlib if we want.

view this post on Zulip Gaëtan Gilbert (Apr 07 2023 at 19:17):

how do you get coqc to treat stdlib as -Q? I guess you have to avoid -coqlib?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:17):

There are 4 special paths now due to the stdlib as documented in corresponding Coq issues:

So I guess we'll do a flag that when off requires users to both add Coq to their list of theories and From Coq Require Import Prelude or any other lib.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:18):

Gaëtan Gilbert said:

how do you get coqc to treat stdlib as -Q? I guess you have to avoid -coqlib?

@Gaëtan Gilbert in the current PR coqc is always called with -boot

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:18):

all libraries are the same for the internal Dune lib DB

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:19):

except the above 4 cases

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:19):

the way it works is not too complex, a Coq library database has a field for a theory that is the stdlib if detected

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:19):

detection works as in Coq

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:20):

at some point once the Dune code is stable we will hopefully share all that logic (as coq-lsp has a full copy of that logic too)

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:22):

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 19:34):

do you need theories mathcomp or theories mathcomp.installed? The linked PR docs seem to disagree on this

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:36):

You use the same name, I guess Ali tried to highlight that the theory was installed.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:36):

It is not easy to document this stuff, as OCaml users know.

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 19:36):

ack, sorry for the dup

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 19:37):

Maybe the main changes to tell users are, when you bump to coq-lang 0.8 two things happen:

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 19:42):

honestly, I'd still like a definition of the user-contrib -> DB function

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 19:43):

does user-contrib/foo/bar/baz always let me use theories foo.bar.baz (hence also theories foo.bar and theories foo?)

view this post on Zulip Paolo Giarrusso (Apr 07 2023 at 19:44):

maybe I'll just ask @Rodolphe Lepigre to test this

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 20:08):

the definition is simple, should be in the docs

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 20:08):

each subdir gets a theory

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 20:08):

yes, you can use that

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 20:12):

of course if you have your own theories built by dune, you want to use what is in your stanza

view this post on Zulip Karl Palmskog (Apr 08 2023 at 16:59):

if you want to enforce From Coq or equivalent in Dune, the best would be to first establish this as a preferred idiom in Coq itself. For example, Require from Stdlib without Coq could be deprecated.

In my view, it's unfortunate to allow different sets of idioms in Coq itself and its build system...

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2023 at 21:59):

More than enforcing it I was thinking of making it the default for 1.0, but the idea is that you can do (use_stdlib true) and go back to the current behavior.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2023 at 22:00):

Was more of a "cosmetic" thing, there is not reason the stdlib needs to be handled specially

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2023 at 22:00):

in particular when we have several developments active that doesn't use the stdlib

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2023 at 22:00):

As of today you can get that behavior by setting (use_stdlib no), then adding Coq to the list of theories

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2023 at 22:09):

There is really no reason for Dune using -Q by default other than we considered that to be the sane default

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2023 at 22:09):

but we can add a flag for Dune to use -R for some theories

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2023 at 22:10):

So the stdlib getting -Q once it is handled like a regular library is just due to that default, not because anything important

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2023 at 22:45):

For example, Require from Stdlib without Coq could be deprecated.

That would be nice, see issue https://github.com/coq/coq/issues/5257 and https://github.com/coq/coq/issues/16091, last time I tried the code made it difficult to implement, maybe it is easier now.

Personally the way I'd go about this to first finish the loadpath unification, then implement the deprecation.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2023 at 22:48):

The main trouble is that actually we want to preserve -R _only_ for the actual compiling library, but that is easier than I had thought actually.

The logic would go like-R is allowed, but only if the module under compilation in that logical path.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2023 at 22:48):

otherwise warning

view this post on Zulip Théo Zimmermann (Apr 11 2023 at 08:58):

As long as the documentation is clear enough and that you can copy-paste some boilerplate to have Stdlib in scope and the prelude loaded by default (i.e., the boilerplate contains (coq.flags -rifrom Coq Prelude) or something like that), then I wouldn't mind going as far as changing the default behavior to not even load the prelude. But it seems best to do this change in a Coq lang version < 1.0 so that you can evaluate the backlash and still have a possibility to revert for 1.0.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2023 at 09:27):

@Théo Zimmermann I was thinking more of just (use_stdlib true) setting.

But indeed very good points; IMHO the experiment is worthwhile, at some point we need to deprecate the implict nature of the Coq namespace, so given that upcoming (coq lang 0.8) is really 1.0 beta, maybe you are right and it makes sense to already set the default there, and try to understand the backslash. 0.8 will already be not very compatible for those using deps in user-contrib, so maybe it is best to do all the changes in a single bump instead of forcing users to go thru 2 steps.

WDYT?

On the backslash side I'd be suprised if someone would find that adding From Coq to the stdlib imports makes their life harder, on the contrary that seems like an improvement in all cases, the logic now would be:

It is a small thing but IMHO helps

view this post on Zulip Karl Palmskog (Apr 11 2023 at 09:30):

if From Coq is better, then I think it makes even more sense to deprecate non-prefixing of Coq inside Coq proper

view this post on Zulip Karl Palmskog (Apr 11 2023 at 09:31):

if you break something that's already deprecated, that's better backlash-wise in my view

view this post on Zulip Gaëtan Gilbert (Apr 11 2023 at 09:33):

From => comes not from your theory
Without From => file in your theory

That is not actually enforced though, you can still do Require Coq.Init.Logic. even when stdlib is with -Q

view this post on Zulip Paolo Giarrusso (Apr 11 2023 at 10:15):

doing a change in Coq lets you reuse all the warning technical infrastructure and deprecation social infrastructure — line numbers, -w -/-w +, deprecation period, ...

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2023 at 10:19):

Yup doing a change in Coq would be great, but I'm afraid that's a lot more work

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2023 at 10:19):

Gaëtan Gilbert said:

From => comes not from your theory
Without From => file in your theory

That is not actually enforced though, you can still do Require Coq.Init.Logic. even when stdlib is with -Q

Yes, good point. So the correct statement is weaker.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2023 at 10:20):

Karl Palmskog said:

if you break something that's already deprecated, that's better backlash-wise in my view

There is not breaking per-se, just config options

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2023 at 10:22):

I am fine having the default (stdlib yes) , if there is a good motivation

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2023 at 10:23):

We already did all the hard work in Dune so a sensible theory database is built

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2023 at 10:24):

Coq is in the database if a stdlib can be found

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2023 at 10:24):

so all the flag does is to add Coq by default to (theories ), and mark it implicit

view this post on Zulip Ali Caglayan (Apr 20 2023 at 18:16):

Composition for installed theories has been merged, it will be available in Dune 3.8 next week

view this post on Zulip Emilio Jesús Gallego Arias (Apr 21 2023 at 13:42):

A nice property of this PR is that it will avoid Coq scanning the whole user-contrib setup if you are only using a part of it. That could provide from little to significant speedups depending on the scenario


Last updated: May 19 2024 at 18:02 UTC