Mario Carneiro (Dec 15 2023 at 12:15): 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
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
Pierre Roux (Dec 15 2023 at 12:20):eval $(opam env --switch=foo --set-switch) sets the switch locally in the current shell
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?
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
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)
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)
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
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)
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 alean-toolchainfile in the project to indicate which version they want)
Looks a lot like what the nix toolbox offers.
Mario Carneiro (Dec 15 2023 at 12:29):I think so, except that it's not nix so it works on windows too
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 toeval $(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
Mario Carneiro (Dec 15 2023 at 12:31):It just puts eval $(opam env) in your .bash-profile or equivalent
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
Johannes Hostert (Dec 15 2023 at 12:54):Mario Carneiro said:
It just puts
eval $(opam env)in your.bash-profileor 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.
Mario Carneiro (Dec 15 2023 at 12:54):oh, good point
Yann Leray (Dec 15 2023 at 12:55):When the opam integration works, the switch gets set dynamically when you change cwd
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.
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.
Karl Palmskog (Dec 15 2023 at 14:21):emacs has this for opam: https://github.com/ProofGeneral/opam-switch-mode
Mario Carneiro (Dec 15 2023 at 14:22):is this information in _CoqProject?
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 ?
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?
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
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.
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
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:
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
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"
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
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
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/
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?
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
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
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.
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
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
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
Mario Carneiro (Dec 15 2023 at 14:40):and that doesn't even have to be a recommended build tool, metadata alone is sufficient
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
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?
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
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
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
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?
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.
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
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
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.
Mario Carneiro (Dec 15 2023 at 14:49):Does this mean that the template builds on coq 0.8?
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
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.
Mario Carneiro (Dec 15 2023 at 14:50):I see. So how does dune know what version of coq to use?
Mario Carneiro (Dec 15 2023 at 14:51):oh, the .opam file does have a "coq" {>= "8.14"} line
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
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.
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.
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
Paolo Giarrusso (Dec 15 2023 at 18:02):And in a theorem prover, changing most definitions is an API break
Paolo Giarrusso (Dec 15 2023 at 18:03):Anyway, "better backwards compat" is a separate thread in any case.
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)
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
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
Paolo Giarrusso (Dec 15 2023 at 18:06):If that happens, the same opam binary can mostly compile any project.
Mario Carneiro (Dec 15 2023 at 18:06):so I should grep the .github/ci.yml file then?
Paolo Giarrusso (Dec 15 2023 at 18:07):"opam files in the source repo" is the closest thing to a programmatic interface
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
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
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.
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
Paolo Giarrusso (Dec 15 2023 at 18:10):Hm, why does the project layout matter here?
Paolo Giarrusso (Dec 15 2023 at 18:11):I've also learned to distrust opam's solver for a bunch of reasons
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)
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
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
Paolo Giarrusso (Dec 15 2023 at 18:12):opam would fail to solve the constraints, if you use a correct workflow
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
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?
Mario Carneiro (Dec 15 2023 at 18:15):I'm not entirely sure I diagnosed the problem correctly
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
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
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
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?
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
Mario Carneiro (Dec 15 2023 at 18:20):but the error message mentioned 4.14 and 4.12
Paolo Giarrusso (Dec 15 2023 at 18:21):If you browse with a switch, build with the same switch
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
Paolo Giarrusso (Dec 15 2023 at 18:21):The OCaml vscoq plugin already lets you select switch per project
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
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
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
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
Yann Leray (Dec 15 2023 at 18:25):Why do you need more than one OCaml version ?
Mario Carneiro (Dec 15 2023 at 18:25):beats me, I didn't design this build nightmare
Paolo Giarrusso (Dec 15 2023 at 18:26):
Mario Carneiro (Dec 15 2023 at 18:26):I just follow instructions and then complain when they don't work
Mario Carneiro (Dec 15 2023 at 18:26):and then incredibly helpful people come out of the woodwork and make it actually work :)
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
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
Mario Carneiro (Dec 15 2023 at 18:28):I also see something like that
Paolo Giarrusso (Dec 15 2023 at 18:28):second item lists "opam switches" :-)
Mario Carneiro (Dec 15 2023 at 18:28):oh nice, my coq.8.16 switch has coq 8.18 installed on it
Paolo Giarrusso (Dec 15 2023 at 18:29):indeed, switch names are just comments
Paolo Giarrusso (Dec 15 2023 at 18:30):(not literally, but opam should respect alpha-renaming switches, so this can happen)
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
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
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
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
Mario Carneiro (Dec 15 2023 at 18:35):I assure you I have no idea how to do that
Paolo Giarrusso (Dec 15 2023 at 18:35):agreed here with both Yann and Mario :-)
In general:
opam switch link before building, then the appropriate switch to use is at least recorded so that the editor _may_ use it (OCaml editors do, but no Coq editor does that today AFAIK) Mario Carneiro (Dec 15 2023 at 18:36):if only the editor could read your file instead...
Paolo Giarrusso (Dec 15 2023 at 18:36):but without opam switch link, that makes no sense
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)
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
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
Mario Carneiro (Dec 15 2023 at 18:40):ah, so it does. It makes it sound more optional than it is
Paolo Giarrusso (Dec 15 2023 at 18:40):well, it is optional
Mario Carneiro (Dec 15 2023 at 18:41):it is required for certain use cases
Paolo Giarrusso (Dec 15 2023 at 18:41):nope
Paolo Giarrusso (Dec 15 2023 at 18:41):I can have a single switch, or I can have multiple switches and tell my editor
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.
Paolo Giarrusso (Dec 15 2023 at 18:42):But IME, neither OCaml nor Coq is like that today.
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)
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
Paolo Giarrusso (Dec 15 2023 at 18:44):ugh
Paolo Giarrusso (Dec 15 2023 at 18:44):"ugh" as in "who thought committing .vscode files was a good idea"
Mario Carneiro (Dec 15 2023 at 18:44):who thought it would be a good idea to make every editor reimplement the build logic
Paolo Giarrusso (Dec 15 2023 at 18:45):that file replicates part of _CoqProject as well
Yann Leray (Dec 15 2023 at 18:45):They are required for the arguments, since _CoqProject isn't picked up from our tests
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
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
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
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
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.
Paolo Giarrusso (Dec 15 2023 at 18:50):@Yann Leray well, but then Mario's right that the README is incomplete
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
Paolo Giarrusso (Dec 15 2023 at 18:51):makes sense — the build turns _CoqProject.in into _CoqProject I guess
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.
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)
Paolo Giarrusso (Dec 15 2023 at 19:04):I mean, the actual bug here is about building Coq code
Paolo Giarrusso (Dec 15 2023 at 19:05):the opam build files are complete
Mario Carneiro (Dec 15 2023 at 19:05):I'm not sure what you mean by that
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
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.
Paolo Giarrusso (Dec 15 2023 at 19:07):and metacoq only needs that because of accidents/limitations with _CoqProject that are fixed by dune.
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.
Mario Carneiro (Dec 15 2023 at 19:10):Is it possible to test whether a switch could compile the project?
Paolo Giarrusso (Dec 15 2023 at 19:11):checking deps match is roughly something like opam --switch $target_switch install --dry-run <opam files>
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
Mario Carneiro (Dec 15 2023 at 19:13):in which case you could do something like:
opam switch link so that it doesn't prompt next time Paolo Giarrusso (Dec 15 2023 at 19:14):wait.
Paolo Giarrusso (Dec 15 2023 at 19:14):who installs the missing deps?
Mario Carneiro (Dec 15 2023 at 19:14):opam I guess?
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)
Mario Carneiro (Dec 15 2023 at 19:15):yikes
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
Mario Carneiro (Dec 15 2023 at 19:15):well that's why it's a prompt and not just a done deal
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
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.
Paolo Giarrusso (Dec 15 2023 at 19:17):"just a package deal"?
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
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
Paolo Giarrusso (Dec 15 2023 at 19:19):it sounds like opam is split across elan + lake?
Paolo Giarrusso (Dec 15 2023 at 19:20):elan for the compiler and lake for packages?
Mario Carneiro (Dec 15 2023 at 19:20):opam is lake, elan doesn't exist AFAICT
Paolo Giarrusso (Dec 15 2023 at 19:20):opam will install ocamlc from source
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)
Mario Carneiro (Dec 15 2023 at 19:21):lake builds dependencies from source, elan is binary distribution
Paolo Giarrusso (Dec 15 2023 at 19:21):no binary distribution in opam, indeed
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
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?
Mario Carneiro (Dec 15 2023 at 19:22):you could do a similar architecture either way
Mario Carneiro (Dec 15 2023 at 19:22):Each switch has another compiler and all dependencies
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
Mario Carneiro (Dec 15 2023 at 19:24):the switches are the toolchains
Paolo Giarrusso (Dec 15 2023 at 19:24):so, I can create two toolchains with the same compiler?
Mario Carneiro (Dec 15 2023 at 19:25):the toolchain contains the compiler in the package
Mario Carneiro (Dec 15 2023 at 19:25):I suppose you could symlink stuff if you are short on space but generally no
Paolo Giarrusso (Dec 15 2023 at 19:25):oh, I'm ambiguous too.
Mario Carneiro (Dec 15 2023 at 19:25):if this was a major concern I can imagine elan doing it transparently
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.
Mario Carneiro (Dec 15 2023 at 19:26):but with lean the main reason you need another switch/toolchain is because the compiler changed
Mario Carneiro (Dec 15 2023 at 19:26):Oh yes you can do that
Mario Carneiro (Dec 15 2023 at 19:26):but lean doesn't depend on lib-foo
Paolo Giarrusso (Dec 15 2023 at 19:26):I assume my projects depend on different versions of lib-foo
Mario Carneiro (Dec 15 2023 at 19:27):yes, it would be lake handling that
Mario Carneiro (Dec 15 2023 at 19:27):which maybe is similar to dune here?
Mario Carneiro (Dec 15 2023 at 19:27):it builds lean projects including dependencies
Paolo Giarrusso (Dec 15 2023 at 19:28):today that's similar to opam
Paolo Giarrusso (Dec 15 2023 at 19:28):I'm ignoring the dune-opam integration because I haven't looked into it
Mario Carneiro (Dec 15 2023 at 19:29):Is dune the newfangled thing that hasn't caught on then?
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)
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
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
Paolo Giarrusso (Dec 15 2023 at 19:30):every OCaml project uses dune these days, while few Coq projects do yet
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?
Mario Carneiro (Dec 15 2023 at 19:32):I assume metacoq is doing something like that
Paolo Giarrusso (Dec 15 2023 at 19:32):it depends
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
Paolo Giarrusso (Dec 15 2023 at 19:33):maybe in Lean you _can't_ install dependencies globally?
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
Mario Carneiro (Dec 15 2023 at 19:34):which means you will end up with two toolchains if you compile both
Paolo Giarrusso (Dec 15 2023 at 19:34):no, I'm assuming they both use lean v4.1
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
Mario Carneiro (Dec 15 2023 at 19:35):so if they are both using v4.1 then there is only one switch
Paolo Giarrusso (Dec 15 2023 at 19:35):well, that sounds like lean doesn't support my scenario
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?
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
Mario Carneiro (Dec 15 2023 at 19:36):That's right, you can't install external projects on the toolchain
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)
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?
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
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)
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
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
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
Paolo Giarrusso (Dec 15 2023 at 19:41):so, _any artifact_ is either a toolchain _or_ locally installed?
Mario Carneiro (Dec 15 2023 at 19:41):right now, yes
Paolo Giarrusso (Dec 15 2023 at 19:41):okay, so toolchains are more restricted compared to opam switches
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
Mario Carneiro (Dec 15 2023 at 19:42):I think that would make it similar to nix
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
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
Paolo Giarrusso (Dec 15 2023 at 19:46):that "antipattern" is necessary unless you solve nontrivial problems
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
Mario Carneiro (Dec 15 2023 at 19:47):The solution to the nontrivial problem is a file like this, it's not rocket science
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
Paolo Giarrusso (Dec 15 2023 at 19:48):but that's not the problem
Mario Carneiro (Dec 15 2023 at 19:49):that solves the eval $(opam env) problem
Paolo Giarrusso (Dec 15 2023 at 19:49):no
Paolo Giarrusso (Dec 15 2023 at 19:49):you can write an opam file listing all dependencies
Mario Carneiro (Dec 15 2023 at 19:49):so why can't my tooling figure it out?
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
Paolo Giarrusso (Dec 15 2023 at 19:50):you explained how it could work today
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.
Paolo Giarrusso (Dec 15 2023 at 19:51):let alone a switch fitting the constraints of two projects.
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)
Paolo Giarrusso (Dec 15 2023 at 19:52):if we ignored space and build time, it would.
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.
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)
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.
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
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.
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.
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
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:
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.
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.
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.
Mario Carneiro (Dec 15 2023 at 20:01):or you could download binaries
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
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.
Mario Carneiro (Dec 15 2023 at 20:03):system dependencies meaning what exactly?
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.
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.
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 :-)
Paolo Giarrusso (Dec 15 2023 at 20:05):but yeah, you could often set aside system deps in practice
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
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.
Paolo Giarrusso (Dec 15 2023 at 20:07):all that is part of binaries
Alex Sanchez-Stern (Dec 15 2023 at 20:07):Ah sure, binaries as in vo files.
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)
Paolo Giarrusso (Dec 15 2023 at 20:08):but stuff like jump-to-definition requires compiled .glob and source .v files
Mario Carneiro (Dec 15 2023 at 20:08):but it doesn't take half an hour to install because it's unzipping not building
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.
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.
Paolo Giarrusso (Dec 15 2023 at 20:09):for soundness you needn't rebuild from source
Mario Carneiro (Dec 15 2023 at 20:09):yes, there is a separate tool for rechecking (I think this is coqchk?)
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
Mario Carneiro (Dec 15 2023 at 20:10):for the truly paranoid, no switch is enough :)
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
Mario Carneiro (Dec 15 2023 at 20:11):ideally you would be able to use metacoq as a .vo checker
Alex Sanchez-Stern (Dec 15 2023 at 20:12):Ah, sounds "trivial" then :laughing:
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:
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
Paolo Giarrusso (Dec 15 2023 at 20:15):but this is OT
Paolo Giarrusso (Dec 15 2023 at 20:15):binary distribution for Coq is blocked on binary distribution for OCaml
Paolo Giarrusso (Dec 15 2023 at 20:16):unless you solve both via Docker
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
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: Oct 13 2024 at 01:02 UTC