Stream: Coq users

Topic: Per-folder opam switch?


view this post on Zulip Mario Carneiro (Dec 15 2023 at 12:15):

Is there a way to set the current opam switch locally to a folder? It seems this command has global effect, which means that I can't work on projects with different requirements at the same time

view this post on Zulip Mario Carneiro (Dec 15 2023 at 12:18):

Concretely: to browse the coq sources I need ocaml 4.14 and to browse metacoq I need coq 8.18 which uses ocaml 4.12. I would like to look at both of them

view this post on Zulip Pierre Roux (Dec 15 2023 at 12:20):

eval $(opam env --switch=foo --set-switch) sets the switch locally in the current shell

view this post on Zulip Mario Carneiro (Dec 15 2023 at 12:23):

I guess there isn't any way to store the information in a file so that I can just run coqc or make or dune or whatever and it just works with the right version?

view this post on Zulip Karl Palmskog (Dec 15 2023 at 12:25):

you may want to look at the Coq Nix Toolbox if you want that kind of functionality

view this post on Zulip Johannes Hostert (Dec 15 2023 at 12:25):

There is opam switch link, which is exactly what you asked for (except that you still need to eval $(opam env) everytime)

view this post on Zulip Mario Carneiro (Dec 15 2023 at 12:26):

I am spoiled by elan, which just makes this work out of the box (people put a lean-toolchain file in the project to indicate which version they want)

view this post on Zulip Mario Carneiro (Dec 15 2023 at 12:27):

opam switch link is a good solution for me personally, although it's not something I can commit to a project IIUC

view this post on Zulip Johannes Hostert (Dec 15 2023 at 12:27):

You can also create a local-only switch using opam switch create ., and you can even symlink them around (if you have different developments that need the same switch)

view this post on Zulip Pierre Roux (Dec 15 2023 at 12:28):

Mario Carneiro said:

I am spoiled by elan, which just makes this work out of the box (people put a lean-toolchain file in the project to indicate which version they want)

Looks a lot like what the nix toolbox offers.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 12:29):

I think so, except that it's not nix so it works on windows too

view this post on Zulip Ana de Almeida Borges (Dec 15 2023 at 12:30):

Johannes Hostert said:

There is opam switch link, which is exactly what you asked for (except that you still need to eval $(opam env) everytime)

this, but IIRC there is something you can add to your shell configuration to avoid having to do eval $(opam env) every time. I think opam offers to do it for you when you install it

view this post on Zulip Mario Carneiro (Dec 15 2023 at 12:31):

It just puts eval $(opam env) in your .bash-profile or equivalent

view this post on Zulip Mario Carneiro (Dec 15 2023 at 12:36):

I now see what the _opam folder here was about. It would be nice if this opam switch link invocation was mentioned in project setup instructions if it is recommended

view this post on Zulip Johannes Hostert (Dec 15 2023 at 12:54):

Mario Carneiro said:

It just puts eval $(opam env) in your .bash-profile or equivalent

Yes, and that's unfortunately not good enough unless there is a way to execute it whenever you cd, since your opam switch now depends on your current directory.
And even then, sometimes I want to cd without this getting in the way.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 12:54):

oh, good point

view this post on Zulip Yann Leray (Dec 15 2023 at 12:55):

When the opam integration works, the switch gets set dynamically when you change cwd

view this post on Zulip Michael Soegtrop (Dec 15 2023 at 13:10):

Another way: in VSCoq you can choose the opam switch (the coqc bin folder) per project or folder. This will switch all coq tools, but no other things you might have in opam, so it is not quite the same as setting an opam switch.

view this post on Zulip Arnaud DABY-SEESARAM (Dec 15 2023 at 14:11):

In more complex setups (e.g. if you have other envars to export or if you edit several projects at once), you can also use direnv, which integrates with bash/zsh/...
It allows you to updates the current environment variables on the fly (what opam env does) depending on your directory.
NB : there is a mode for direnv in emacs and a similar thing for VSCode.

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:21):

emacs has this for opam: https://github.com/ProofGeneral/opam-switch-mode

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:22):

is this information in _CoqProject?

view this post on Zulip Arnaud DABY-SEESARAM (Dec 15 2023 at 14:23):

Karl Palmskog said:

emacs has this for opam: https://github.com/ProofGeneral/opam-switch-mode

Is there a way to set it up automatically for a given directory (like with directory variables or something similar) such that switching between two buffers living in different projects updates the opam switch automatically ?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:25):

Oh I noticed that the version is listed in e.g. https://github.com/MetaCoq/metacoq/blob/coq-8.18/coq-metacoq-pcuic.opam . Is this file standard practice?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:29):

maybe not, seems like that's just a project local name and not something you can give to opam

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:29):

Arnaud DABY-SEESARAM said:

Karl Palmskog said:

emacs has this for opam: https://github.com/ProofGeneral/opam-switch-mode

Is there a way to set it up automatically for a given directory (like with directory variables or something similar) such that switching between two buffers living in different projects updates the opam switch automatically ?

No idea, you could try asking in the #Proof General users stream.

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:30):

in opam, one can define the version or omit it, depending on what is most convenient for order sorting

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:30):

Would it be unreasonable to ask for some standardized way of putting the coq version in git repos so that tools can pick up on it? :sad:

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:32):

Coq and opam are distinct. The canonical versions of packages live in our opam repo (and in a corresponding Nix repo): https://github.com/coq/opam

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:33):

I am reminded of a talk at this year's ITP which was nominally about testing a proof repair tool on coq projects but was actually 80% "how to figure out how to compile coq projects in the wild"

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:33):

anyone who builds from repos are effectively on their own, the standard recommendation is to use the Coq Platform

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:34):

they were trying to build projects across 10+ Coq versions, without any reference to their opam packages or other metadata

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:35):

for advanced users, we maintain a set of Git-based opam packages (again Nix has its own): https://github.com/coq/platform/

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:35):

are "opam packages and other metadata" sufficient to reliably and automatically orient oneself in a git repo which follows current best practices?

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:36):

there are many forms of "best practices". Some people have an opam package in their repo, some don't

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:38):

I don't know what that means. Let's say this is a coq project, with coq source files that one expects to be able to compile. Can we figure out how to do that? I don't know whether this entails it being an "opam package", I don't think it does

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:38):

some people build everything with Dune, some use from-scratch Makefiles, some use coq_makefile-generated Makefiles. We recommend people to do and rely on releases instead of relying on master/main from a repo. The Coq Platform is effectively one big tested release of most utility packages one can want.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:39):

my focus is on source repos because I want to look at the code not just refer to it

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:39):

there is no one single way to build every Coq project. The situation is similar for OCaml and similar languages - the language is distinct from package/repo management

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:40):

Okay, but that doesn't mean you can't have a recommendation which is followed by the big projects

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:40):

and that doesn't even have to be a recommended build tool, metadata alone is sufficient

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:41):

we maintain various recommendations and tools in Coq-community for maintaining a Coq project: https://github.com/coq-community/templates

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:42):

Since you brought up the Coq Platform: is it the case that we can automatically determine how to build projects on the Coq Platform from source?

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:42):

but that [having recommendations] doesn't really mean that people follow them. CompCert is a commercial product, they will build it however they want. But they publish opam packages to the Coq opam archive which makes it possible to include in the Coq Platform

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:43):

the Coq Platform is based on opam, which at its core is a tool for building from source

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:43):

sure, once you have a recommendation it's a complex social situation whether it actually gets adopted in practice

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:44):

the closest thing that I've seen to a project file so far is _CoqProject, although it seems to be makefile generated?

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:45):

it's not generated typically. It's a convention to have a _CoqProject file since editors can use it to determine the logical path of a Coq project, such as compcert.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:46):

yes, that's what I'm talking about. "Editors break if you don't use it" is a great motivator to set things up appropriately

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:46):

if there is a list of files in _CoqProject, it can be handed to coq_makefile to generate the Makefile. I compare different ways to build Coq projects here: https://github.com/coq-community/coq-program-verification-template#building-instructions

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:48):

OCaml recently said they will eventually use Dune to build+interact with anything OCaml. It's not unlikely Coq will follow in OCaml's footsteps eventually, but right now Dune doesn't support all editor workflows.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:49):

Does this mean that the template builds on coq 0.8?

view this post on Zulip Gaëtan Gilbert (Dec 15 2023 at 14:49):

Mario Carneiro said:

the closest thing that I've seen to a project file so far is _CoqProject, although it seems to be makefile generated?

it's the other way around, coq_makefile generates makefiles from _coqproject files

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:50):

coq 0.8 is the Coq support level in the Dune build tool. It signifies what features are available when building Coq projects. It's mostly indendent of the Coq version.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:50):

I see. So how does dune know what version of coq to use?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 14:51):

oh, the .opam file does have a "coq" {>= "8.14"} line

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:51):

Dune works the same as opam by default, it uses coqc from the PATH. It can be configured to use another one, of course

view this post on Zulip Karl Palmskog (Dec 15 2023 at 14:52):

it seems the OCaml people have decided that projects should generate their .opam files from their dune-project files (dune build does this generation automatically when opam metadata is declared). Coq projects can also do this, but typically don't.

view this post on Zulip Stefan Monnier (Dec 15 2023 at 15:50):

While all these tools to specify and manage version dependencies are quite handy, I find it sad to see how little effort is spent comparatively on improving support for compatibility across versions.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:01):

Coq already has much stronger backwards compat than Lean, which already enshrines for years behavior that is known to be bonkers

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:02):

And in a theorem prover, changing most definitions is an API break

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:03):

Anyway, "better backwards compat" is a separate thread in any case.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:05):

On the other hand, elan is very stable, which means you can jump into any lean project and compile it using the same elan binary (which fetches the appropriate version of lean if needed)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:05):

@Mario Carneiro I'd say the only unofficial recommendation is yo provide opam packages, ideally also as part of the source repository, and ideally even test them in CI

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:06):

but in coq I don't see how one could even write such a program because there isn't any clean alternative to the lean-toolchain file except grepping the readme

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:06):

If that happens, the same opam binary can mostly compile any project.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:06):

so I should grep the .github/ci.yml file then?

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:07):

"opam files in the source repo" is the closest thing to a programmatic interface

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:08):

is it something an editor could parse, or do you need to ask opam to give you the information

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:08):

Something like "opam switch create ." (and/or specifying the opam packages) might be close to what you want, except I think it's too wasteful

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:09):

but if you're willing to rebuild opam and coqc for each project, it might mostly work.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:09):

yes, the trouble with relying on build tools for project configuration is that build tools like building things, and usually querying the project layout is not a high priority

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:10):

Hm, why does the project layout matter here?

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:11):

I've also learned to distrust opam's solver for a bunch of reasons

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:11):

well, the location of source files is also important (but this is already mostly covered by _CoqProject)

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:12):

metacoq has a whole collection of .opam files. I can't imagine what would happen if they describe different coq versions

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:12):

"what are the external dependencies" (opam files) and "how to find sources/internal dependencies" (_CoqProject) are orthogonal questions today

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:12):

opam would fail to solve the constraints, if you use a correct workflow

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:13):

It's not the case that opam install a b can be split into opam install a; opam install b — that's not true with any package manager (outside Nix, because the question doesn't make sense), but opam is especially bad at it

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:15):

For your original question, BTW, did anybody point out Coq 8.18 works on opam 4.14?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:15):

I'm not entirely sure I diagnosed the problem correctly

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:16):

I tried to browse the coq sources with the coq.8.18 switch enabled after having previously compiled it with whatever dev version was in use, and the vscode ocaml plugin started complaining about a version mismatch

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:19):

That description is very incomplete, but IME no two distinct Coq binaries can exchange .vo files, and this might or might not be relevant

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:20):

the issue happened in the ocaml plugin because I was looking at .ml files from the coq sources

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:20):

Well, if you mixed ocaml 4.14 and .12 as you said, that'd explain it, no?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:20):

I don't really know how to determine the ocaml version <-> coq version mapping so I made a best guess

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:20):

but the error message mentioned 4.14 and 4.12

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:21):

If you browse with a switch, build with the same switch

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:21):

well yes, I agree with that and the error is most logical. But global switches make no sense in this context hence the question

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:21):

The OCaml vscoq plugin already lets you select switch per project

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:22):

For Coq plugins, you can give the path to the Coq binary, and you'd typically give a path to the binary in the right switch

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:24):

the vscode plugin is "OCaml Platform", it's pretty good but I don't see anything directly referencing opam in the preferences

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:24):

it seems to work with opam switch link well enough so that's what I'm doing

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:24):

I'm not judging if this is ideal — it probably isn't — but it can be handled by managing things manually...
Let me screenshot the right pane, it's not in the preferences

view this post on Zulip Yann Leray (Dec 15 2023 at 18:25):

Why do you need more than one OCaml version ?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:25):

beats me, I didn't design this build nightmare

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:26):

image.png

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:26):

I just follow instructions and then complain when they don't work

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:26):

and then incredibly helpful people come out of the woodwork and make it actually work :)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:26):

@Yann Leray dependencies can vary, so one needs different switches, and for each switch something must pick the version

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:27):

@Mario Carneiro as you see, I clicked on the "OCaml" button on the left bar, and then all that stuff shows up for me

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:28):

I also see something like that

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:28):

second item lists "opam switches" :-)

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:28):

oh nice, my coq.8.16 switch has coq 8.18 installed on it

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:29):

indeed, switch names are just comments

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:30):

(not literally, but opam should respect alpha-renaming switches, so this can happen)

view this post on Zulip Yann Leray (Dec 15 2023 at 18:30):

I'm not sure I understand, recent enough versions of Coq support all modern versions of OCaml, so sticking to either 4.14 or 5 should do.
The installation for source is opam install . --deps-only and if there is a conflict you create another (possibly local) switch; at least that's how I do

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:31):

@Yann Leray yes, and unless you manually pick the same OCaml version for all such switches, you can get a different OCaml version for each switch

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:32):

but not sure it matters much — I wouldn't try to exchange binary artifacts across two switches, just because they have the same OCaml

view this post on Zulip Yann Leray (Dec 15 2023 at 18:34):

Going back to the first message, you can have a single switch to browse both Coq and MetaCoq, since their dependencies overlap

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:35):

I assure you I have no idea how to do that

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:35):

agreed here with both Yann and Mario :-)
In general:

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:36):

if only the editor could read your file instead...

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:36):

but without opam switch link, that makes no sense

view this post on Zulip Yann Leray (Dec 15 2023 at 18:37):

MetaCoq makes VSCode read from the local switch; if it is linked through opam switch link it should work. Does it not ? (I have a local switch there and it works fine)

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:38):

it does, except that the readme doesn't say anything about setting up a local switch so it just fails because _opam is missing

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:39):

@Mario Carneiro https://github.com/MetaCoq/metacoq/blob/coq-8.16/INSTALL.md#setting-up-an-opam-switch mentions both local switches and opam switch link

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:40):

ah, so it does. It makes it sound more optional than it is

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:40):

well, it is optional

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:41):

it is required for certain use cases

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:41):

nope

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:41):

I can have a single switch, or I can have multiple switches and tell my editor

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:42):

let me say this: it's nice if in Lean you needn't worry about any of this.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:42):

But IME, neither OCaml nor Coq is like that today.

view this post on Zulip Yann Leray (Dec 15 2023 at 18:43):

It is the usual way to ensure VSCode knows where to look for vscoq/coq-lsp, but is not the only one. You could change the path from the editor instead (and would probably have to for other editors than VSCode)

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:43):

Paolo Giarrusso said:

I can have a single switch, or I can have multiple switches and tell my editor

That's what I tried, and it fails because the vscode config makes explicit reference to _opam

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:44):

ugh

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:44):

"ugh" as in "who thought committing .vscode files was a good idea"

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:44):

who thought it would be a good idea to make every editor reimplement the build logic

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:45):

that file replicates part of _CoqProject as well

view this post on Zulip Yann Leray (Dec 15 2023 at 18:45):

They are required for the arguments, since _CoqProject isn't picked up from our tests

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:46):

@Mario Carneiro you're implying editor-build integration was designed organically, I'm afraid that's not true

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:46):

it looks very much like the editors came on the scene late and had to make the best of a very haphazard world

view this post on Zulip Yann Leray (Dec 15 2023 at 18:47):

Mario Carneiro said:

Paolo Giarrusso said:

I can have a single switch, or I can have multiple switches and tell my editor

That's what I tried, and it fails because the vscode config makes explicit reference to _opam

You can have a single switch, link it locally and it would work

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:47):

@Yann Leray if you open workspace foo, then _CoqProject is loaded by default from that folder — that's tweakable by customizing coq.coqProjectRoot

image.png

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:49):

so, either open each folder, or have a _CoqProject in the MetaCoq root just for use by the editors.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:50):

@Yann Leray well, but then Mario's right that the README is incomplete

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:50):

Note that it works fine if you open the subfolders, the .vscode thing seems to be working around issues with the "workspace" structure of the metacoq repo

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:51):

makes sense — the build turns _CoqProject.in into _CoqProject I guess

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 18:53):

and there's a genuine problem — the _CoqProject I suggest isn't the right one for building (since it allows any library to depend on any other); today you need dune to specify such workspace structure.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 18:56):

Still, even if things are diverse now, I don't see major obstacles with creating a new standard and having it be picked up by the biggest / most well maintained packages, as long as it's just about project structure and metadata and not actual building. But I'm coming from an ecosystem that is significantly more centralized (which BTW relates to why it is less focused on forward/backward compatibility, because we can actually "fix the world", at least for now)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:04):

I mean, the actual bug here is about building Coq code

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:05):

the opam build files are complete

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:05):

I'm not sure what you mean by that

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:06):

most Coq projects have okay docs for building the code itself, but an editor needs to know how to call commands that aren't regular coqc invocations and e.g. may not be in the makefile

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

the only problem with opam is "nothing says you must create a local switch", but the fix is to not rely on the switch being local.

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

and metacoq only needs that because of accidents/limitations with _CoqProject that are fixed by dune.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:09):

Mario Carneiro said:

most Coq projects have okay docs for building the code itself, but an editor needs to know how to call commands that aren't regular coqc invocations and e.g. may not be in the makefile

if you mean "the editor should install dependencies", .opam files give the info on how to do that. If we were all okay with automatically creating a new opam switch per project, and rebuilding ocaml and coqc each time, we could add support to editors today.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:10):

Is it possible to test whether a switch could compile the project?

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:11):

checking deps match is roughly something like opam --switch $target_switch install --dry-run <opam files>

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:12):

you could then tell the user to run opam --switch $target_switch install <opam files>, but that's a large side effect that I wouldn't want to automate

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:13):

in which case you could do something like:

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:14):

wait.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:14):

who installs the missing deps?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:14):

opam I guess?

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:15):

but running opam --switch $target_switch install isn't safe — opam might at least decide to rebuild other packages, change installed deps, rebuild coqc (breaking binary compat with existing .vo files), maybe uninstall packages (not sure on this)

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:15):

yikes

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:15):

tho I think that's true of _ANY_ package manager with multiple versions of the same package

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:15):

well that's why it's a prompt and not just a done deal

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:17):

in elan toolchains are basically the equivalent of switches, but they are just a package deal, you get the compiler and projects are not managed by the switch

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:17):

that could work. I fear users would click through too easily and suffer, but that already happens today.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:17):

"just a package deal"?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:18):

you get the "core distribution" i.e. lean + lake as binaries, projects are not managed by elan

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:19):

although elan is based on rustup which has a concept of "components" which might be analogous to coq plugins

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:19):

it sounds like opam is split across elan + lake?

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:20):

elan for the compiler and lake for packages?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:20):

opam is lake, elan doesn't exist AFAICT

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:20):

opam will install ocamlc from source

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:20):

(er, it can — it can also use the distro package, but that's IMHO a bad idea for different reasons)

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:21):

lake builds dependencies from source, elan is binary distribution

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:21):

no binary distribution in opam, indeed

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:21):

although I don't think it's an essential difference whether it is binary or builds from source

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:22):

so how do you deal with 2 switches that share ocaml version but have different versions of dependency A?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:22):

you could do a similar architecture either way

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:22):

Each switch has another compiler and all dependencies

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:24):

I'm not sure what you mean — I'm asking if lake gives you some way to have multiple switches on the same toolchain

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:24):

the switches are the toolchains

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:24):

so, I can create two toolchains with the same compiler?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:25):

the toolchain contains the compiler in the package

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:25):

I suppose you could symlink stuff if you are short on space but generally no

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:25):

oh, I'm ambiguous too.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:25):

if this was a major concern I can imagine elan doing it transparently

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:26):

I'm asking if you can create lean.4.0.1, lib-foo.0.1 and lean.4.0.1, lib-foo.0.2.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:26):

but with lean the main reason you need another switch/toolchain is because the compiler changed

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:26):

Oh yes you can do that

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:26):

but lean doesn't depend on lib-foo

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:26):

I assume my projects depend on different versions of lib-foo

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:27):

yes, it would be lake handling that

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:27):

which maybe is similar to dune here?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:27):

it builds lean projects including dependencies

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:28):

today that's similar to opam

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:28):

I'm ignoring the dune-opam integration because I haven't looked into it

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:29):

Is dune the newfangled thing that hasn't caught on then?

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:29):

I just meant that dune's is just a build tool not a package manager (outside of this integration)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:30):

so, installing lib-foo into a switch is opam's job, and building your source project is dune's job

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:30):

lake is mainly a build tool, but it does know how to locate dependencies in git repos

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:30):

every OCaml project uses dune these days, while few Coq projects do yet

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:31):

So if you have two local projects and one depends on the other, do you need to install the dep into your switch to use it downstream?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:32):

I assume metacoq is doing something like that

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:32):

it depends

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:32):

honestly, I'm still missing something, because it's not clear if in Lean you can do opam --switch A install lib-foo.0.1; opam --switch B install lib-foo.0.2

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:33):

maybe in Lean you _can't_ install dependencies globally?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:33):

lib-foo.0.1 says "I use lean v4.1" and lib-foo.0.2 says "I use lean v4.2", and elan makes sure that the right lean is used to compile each project

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:34):

which means you will end up with two toolchains if you compile both

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:34):

no, I'm assuming they both use lean v4.1

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:35):

Like I said, the equivalent of switches are toolchains, there is one toolchain labeled lean v4.1 and another one labeled lean v4.2 and that's what they have in them

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:35):

so if they are both using v4.1 then there is only one switch

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:35):

well, that sounds like lean doesn't support my scenario

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:36):

it's not even clear if you _can_ install lib-foo into the toolchain — if the name is accurate, maybe you can't?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:36):

The whole idea behind this design is to avoid needing to say --switch A, projects tell you what they build on not the other way around

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:36):

That's right, you can't install external projects on the toolchain

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:37):

this may change in the future, but for now elan is just about delivering the core tooling (the build tool and compiler)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:37):

so, if lib-bar and lib-baz depend on lib-foo, it sounds like they can't share the build of lib-foo?

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:38):

if Lean is solving a simpler problem, I'm not surprised the tooling is simpler to use

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:39):

building of lean projects and dependencies among them are handled by lake. There is ongoing work to support build caching in lake but currently there is a cache tool specialized to mathlib, which is by far the largest package (and is everyone's dependency so we need that part to work)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:39):

the reason I ask is because Lean doesn't have a package ecosystem comparable to Coq, so my scenario might be mostly/entirely hypothetical in Lean

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:40):

we're moving towards that direction especially in this latest iteration, so we are taking notes regarding how to scale up here

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:40):

lake will normally just recompile all your dependencies in the project folder, so kinda opam switch create . IIUC

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:41):

so, _any artifact_ is either a toolchain _or_ locally installed?

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:41):

right now, yes

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:41):

okay, so toolchains are more restricted compared to opam switches

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:42):

I hope we can get the build cache stored globally with some kind of content addressing scheme similar to what we use for the mathlib cache

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:42):

I think that would make it similar to nix

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:44):

but I think that installs that follow you around like an opam switch are an antipattern. elan does support this, you can set the default toolchain, but the current recommendation is for everyone to use a lean-toolchain to define a specific version of lean that they use

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:44):

in our world, both nix and dune have some build caching — but nix only caches entire packages, while dune has working caching but doesn't "standardize" builds as much

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:46):

that "antipattern" is necessary unless you solve nontrivial problems

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:47):

arguably, Nix solves them, but the solution doesn't seem simple enough to use for large-scale adoption

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:47):

The solution to the nontrivial problem is a file like this, it's not rocket science

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:48):

literally just put the version you use in a file in a standardized location that can be picked up by tooling

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:48):

but that's not the problem

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:49):

that solves the eval $(opam env) problem

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:49):

no

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:49):

you can write an opam file listing all dependencies

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:49):

so why can't my tooling figure it out?

view this post on Zulip Alex Sanchez-Stern (Dec 15 2023 at 19:50):

For reference, here is the equivalent file in a coq project: https://github.com/uwplse/StructTact/blob/master/coq-struct-tact.opam

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:50):

you explained how it could work today

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:50):

but even if we had auto-downloadable binary Coq packages, that wouldn't automatically synthesize an opam switch fitting your constraints.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:51):

let alone a switch fitting the constraints of two projects.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:51):

Suppose we just create a local switch for every project. Would that not work? (Ignoring that this is a waste of space)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:52):

if we ignored space and build time, it would.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:52):

that doesn't solve "I want to build two projects locally and use them in a third one", and that matters in practice, but let's set that aside to scope the discussion.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:53):

the way I would do that in both rust and lean is to change the project config to use a path dependency to the other local project(s)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:54):

I can't say why this isn't implemented, but ignoring build time isn't such a great solution that somebody will jump to implement it, IMHO.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:54):

Note that I spend way more time debugging stupid build incompatibilities than I spend on build time

view this post on Zulip Alex Sanchez-Stern (Dec 15 2023 at 19:55):

I think Rust gets away with it because they can use aggressive caching, that's just complicated to implement.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:56):

I agree there's definitely a learning curve to opam and build tools to avoid such problems.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 19:57):

sharing build artifacts should be an optimization, it should not change observable behavior and it definitely shouldn't cause an error

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 19:57):

I find opam easy and Nix hard, but YMMV, and I carry far too much cursed knowledge about debugging build issues in general :sweat_smile:

view this post on Zulip Alex Sanchez-Stern (Dec 15 2023 at 19:58):

I think opam supports installing packages from path, right? So it might be implementable with the current metadata from .opam files, you would just need to write an opam wrapper script. The only problem I forsee is that not all projects specify their dependencies very tightly, because they don't have to, chicken-and-egg problem. And caching, while it's just an optimization, is often the difference between usable and completely unusable.

view this post on Zulip Alex Sanchez-Stern (Dec 15 2023 at 20:00):

So, the unfortunate answer might just be "PR's welcome" :). Not that that's very satisfying, but Coq isn't a software product, it's research software. The way things get implemented is that someone gets frustrated enough with them to implement them. The same is true of Lean, but the cultures are different and there is more corporate sponsorship in lean, so there is more resources allocated towards tooling.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:01):

for builds to be really pure, you need to handle system deps as well (like Nix does). Ignoring that, if your package manager wants to rebuild packages transparently, then your editor must at least know how to rebuild your project. Which might take several more hours.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 20:01):

or you could download binaries

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:02):

and those hours are required even with perfect build caching — adding package X might add constraints on a Coq dependency and require rebuilding Coq and everything depending on it

view this post on Zulip Alex Sanchez-Stern (Dec 15 2023 at 20:03):

Hmm, you might be able to ignore the system dependencies problem in the first draft though, I don't usually have to switch system dependencies between coq projects. I just install a few system dependencies when I first install opam, and then everything else just gets built through opam. I've only built about 200 coq packages though, there could be other ones that change the system dependencies I haven't run into.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 20:03):

system dependencies meaning what exactly?

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:04):

the Coq platform picks package versions, so if we had sth like https://github.com/OCamlPro/opam-bin, and storage, one could have binaries for selected package combos.

view this post on Zulip Alex Sanchez-Stern (Dec 15 2023 at 20:04):

System dependencies meaning like, GMP for big-int support. Things you would install through your OS that provide a dynamic library.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:05):

or perl deps for packages using that for their build — but luckily, I think camlp5 isn't used any more :-)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:05):

but yeah, you could often set aside system deps in practice

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:06):

but I'm not confident you can ship an OCaml toolchain without an entire SDK, C headers and all — OCaml _source_ packages definitely don't support that

view this post on Zulip Alex Sanchez-Stern (Dec 15 2023 at 20:07):

In terms of binaries, binaries alone aren't enough in a proof assistant, right? The interface to a proof library isn't just functions, it's a bunch of types based on those functions and definitions that you might need to unfold at the source level to prove things.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:07):

all that is part of binaries

view this post on Zulip Alex Sanchez-Stern (Dec 15 2023 at 20:07):

Ah sure, binaries as in vo files.

view this post on Zulip Mario Carneiro (Dec 15 2023 at 20:08):

yeah, the lean toolchain comes with .olean files (for import) and .lean files (so that go-to-definition works)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:08):

but stuff like jump-to-definition requires compiled .glob and source .v files

view this post on Zulip Mario Carneiro (Dec 15 2023 at 20:08):

but it doesn't take half an hour to install because it's unzipping not building

view this post on Zulip Alex Sanchez-Stern (Dec 15 2023 at 20:09):

So with lean, they basically include the source files so that you can jump to them, but also include their pre-built artifacts so that you don't need to rebuild. That makes sense.

view this post on Zulip Alex Sanchez-Stern (Dec 15 2023 at 20:09):

I guess some people would be worried about some sort of soundness attack, but you could always add a switch for the paranoid.

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:09):

for soundness you needn't rebuild from source

view this post on Zulip Mario Carneiro (Dec 15 2023 at 20:09):

yes, there is a separate tool for rechecking (I think this is coqchk?)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:10):

typechecking the .vo/.olean files is enough in principle, indeed — coqchk does that, altho today's implementation is far from adversary-resistant

view this post on Zulip Mario Carneiro (Dec 15 2023 at 20:10):

for the truly paranoid, no switch is enough :)

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:11):

if I sold you a large proof as .vo files, you should probably bet on me corrupting them

view this post on Zulip Mario Carneiro (Dec 15 2023 at 20:11):

ideally you would be able to use metacoq as a .vo checker

view this post on Zulip Alex Sanchez-Stern (Dec 15 2023 at 20:12):

Ah, sounds "trivial" then :laughing:

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:12):

separate topic, but AFAIK a few more PhDs are needed, to reconcile what Coq does and what we can sanely reason about :sweat_smile:

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:14):

https://github.com/coq/coq/issues/7839 lists challenges with making coqchk safer — the joke about corrupted .vo comes from the same person who filed that issue

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:15):

but this is OT

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:15):

binary distribution for Coq is blocked on binary distribution for OCaml

view this post on Zulip Paolo Giarrusso (Dec 15 2023 at 20:16):

unless you solve both via Docker

view this post on Zulip Mario Carneiro (Dec 15 2023 at 20:18):

Incidentally, I implemented a .vo parser in rust yesterday (and found some bugs in the process). Not sure if I'll make a checker but I'm contemplating it, it seems like a good way to learn what's going on

view this post on Zulip Pierre Roux (Dec 15 2023 at 22:19):

Paolo Giarrusso said:

no binary distribution in opam, indeed

We have this in Nix with cachix.


Last updated: Jun 22 2024 at 15:01 UTC