So this is a problem again for me following this, though possibly for a different reason -- i now do need to work with my local changes to the server, and I have a project compiling fine and working with the released version of lsp. however when i try to open it in the extension dev environment for the vscode extension, it keeps giving me "bad version number" errors and won't actually let me step through the file -- this is while im on an 8.17 switch and the project was explicitly compiled using 8.17 as a requirement in dune. running which coq-lsp
gives me the expected output of path/to/coq-lsp/_build/install/default/bin/coq-lsp
so I'm a little confused about what's going on.
Environment variables differ among processes in complex ways. Can you make vscode print what it thinks PATH is? Printing from the terminal inside isn't the same thing. (Maybe even add a setting to customize which path to use, I think eventually it'll be needed, but I'm not a dev so dunno if Emilio would take this)
Alternatively, depending on the platform, if you close all vscode processes then start vscode from a terminal, that should ensure vscode inherits the environment from that terminal. Otherwise, vscode needs to emulate that by launching a shell and grabbing the default environment https://code.visualstudio.com/docs/supporting/faq#_resolving-shell-environment-fails
so I uninstalled my global lsp so path issues really shouldn’t be an issue, especially if it was able to locate some binary for lsp (because there is only one on my computer)
when you say “make vscode print the path” but not through the terminal do you mean through a print statement in the code or something like that?
the strange thing is that the file loaded fine with my global install, which is also for 8.17 — so in theory they should both function on the same version
You said "an 8.17 switch" — are the code and coq-lsp built against the same coq binary and dependencies? Loading will fail if dependencies differ (Coq checks a checksum of the dependencies). And rebuilding the same source need not produce the same binary.
(there's at least one known bug)
So I've done a make clean for lsp + my library and done the whole compilation setup again; still getting the same error.
Basically it works fine for files that don't depend on imports not from stdlib, but as soon as i try to have dependencies within my files it complains about the version those files were compiled with.
what the really confusing part is is that the released 0.1.6.1+8.17
version works with those files perfectly fine
I guess as a follow up is there an exact definition of the version numbers and what release version they represent? I'm guessing 81700 is just 8.17.0.0 or something but it says it expects 81799 which seems wrong
81799 means "master after 8.17's release" I think — https://github.com/coq/coq/blob/master/tools/configure/configure.ml#L26
can you post the actual error? mostly curious _which_ file has that version number
87199 also appears the version number of coq-lsp's vendored coq, for coq-lsp both master and 0.1.6, while https://github.com/ejgallego/coq-lsp/tree/0.1.6+8.17 lacks the vendor
directory entirely so it is likely using whatever coq version you have installed?
https://github.com/ejgallego/coq-lsp/tree/main/vendor
https://github.com/ejgallego/coq-lsp/tree/0.1.6/vendor
https://github.com/ejgallego/coq/blob/d8db2fd7e6df24d56160651d570603d935dac170/tools/configure/configure.ml#L25-L26
https://github.com/ejgallego/coq/blob/8e0314415cc3cd528fc81bf11075d294179f880a/tools/configure/configure.ml#L25-L26
I should have clarified I'm just a user, but I'd consider porting your changes over a coq-lsp version that matches 8.17 — either the release
https://github.com/ejgallego/coq-lsp/tree/0.1.6.1+8.17, or at least something out of
https://github.com/ejgallego/coq-lsp/tree/v8.17.
git diff 0.1.6 0.1.6+8.17
confirms there are some other small differences, but "use a vendored coq version instead of whatever's installed" seems the biggest one
oh that actually was super helpful, thank you! so I think yeah i have the distribution 8.17 release for coq; and my lsp is just set up to track main
File /path/to/_build/default/Prelim.vo
has bad version number 81700 (expected 81799). It is corrupted or was
compiled with another version of
Coq.
Raised at Exninfo.iraise in file "vendor/coq/clib/exninfo.ml", line 79, characters 4-11
Called from Library.intern_from_file in file "vendor/coq/vernac/library.ml", line 248, characters 11-31
Called from Library.intern_library in file "vendor/coq/vernac/library.ml", line 275, characters 10-28
Called from Library.rec_intern_library in file "vendor/coq/vernac/library.ml", line 299, characters 16-68
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Library.require_library_syntax_from_dirpath in file "vendor/coq/vernac/library.ml", line 402, characters 25-100
Called from Vernacentries.vernac_require in file "vendor/coq/vernac/vernacentries.ml", line 1521, characters 15-80
Called from Vernacextend.vtdefault.(fun) in file "vendor/coq/vernac/vernacextend.ml", line 125, characters 29-33
Called from Vernacinterp.interp_typed_vernac in file "vendor/coq/vernac/vernacinterp.ml", line 20, characters 20-113
Called from Vernacinterp.interp_control.(fun) in file "vendor/coq/vernac/vernacinterp.ml", line 205, characters 24-113
Called from Flags.with_modified_ref in file "vendor/coq/lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "vendor/coq/clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen.(fun) in file "vendor/coq/vernac/vernacinterp.ml", line 257, characters 18-43
Called from Vernacinterp.interp_gen in file "vendor/coq/vernac/vernacinterp.ml", line 255, characters 6-279
Re-raised at Exninfo.iraise in file "vendor/coq/clib/exninfo.ml", line 81, characters 4-38
Called from Coq__Interp.coq_interp in file "coq/interp.ml", line 23, characters 2-29
Called from Coq__Protect.eval_exn in file "coq/protect.ml", line 38, characters 14-17
this is the entire error message, it just looked like a lot so i couldn't even get started on how to interpret it but what you said totally makes sense now
i think actually installing emilio's 8.17 fork of coq itself might fix it from what i'm seeing here? if that doesn't work i'll probably try porting my changes to a non vendored version but i think since it looks like we're moving towards a vendored version.
@Emilio Jesús Gallego Arias do you have documentation anywhere on why this change is being made?
again @Paolo Giarrusso thank you so so much! I've been battling this issue for a couple weeks and would probably have spent even longer trying to fix it. I'll let you know if changing my coq install helps.
Hi @Bhakti Shah I'm sorry you are losing so much time with this annoying issue, don't hesitate to open bugs so we can explain this better.
Indeed you have two choices to build coq-lsp:
Using a vendored pinned dependency works great for main due to reproducibility and ease to hack both in Coq and coq-lsp, but also introduces some pain.
So when you build coq-lsp with a vendored Coq, the coqc used is the one in _build/install/default/bin/coqc
However if you have an opam setup with files in .opam/foo/lib/coq/user-contrib/Uuuuh.vo
that .vo file was compiled with coqc in .opam/foo/bin/coqc
The right solution to this problem --- which I'm hoping to implement soon --- is to have coq-lsp support auto-build of .vo files, so you never ever have this problem again as coq-lsp will detect a .vo is not right and re-build it on the fly.
Meanwhile, you have the following options:
main
branch and "vendor" your Coq libraries too, that is to say, place the sources in vendor/my_coq_lib
and use dune exec -- make
or dune exec -- coqc
etc... to build themmain
branch but use an opam switch: in this case you'll need to pin Coq (and coq-serapi) to coq.dev from the Coq Opam repository, and remove the vendor
directory.v8.17
and opam (and be sure that git removes the vendor
directory).Emilio Jesús Gallego Arias said:
The right solution to this problem --- which I'm hoping to implement soon --- is to have coq-lsp support auto-build of .vo files, so you never ever have this problem again as coq-lsp will detect a .vo is not right and re-build it on the fly.
Hmm, wouldn't this be a little surprising for users if just opening a file with VSCoq or other coq-lsp-based editor caused the vo file to fail with other versions of Coq, or suddenly take longer on another version (because it has to rebuild)? Usually you don't expect your editor to have destructive side effects. Is it possible to have multiple vo files for a particular v file? That way if you already had a .vo from coq 8.15, and then you opened the .v file with coq-lsp on coq 8.17, it could just build a special .vo.17 file and not overwrite the existing vo file.
Yes, indeed coq-lsp will maintain its own binary cache, so that shouldn't be a problem
Sound caching goes beyond keeping track of Coq versions, you also need to keep track of .v file versions, etc...
But certainly it is a priority that coq-lsp users never see again that mismatch problem.
How does auto-build deal with "my code only works on 8.16/8.17/..."?
Autobuilding sources is good for other reasons, but for version mismatches it seems autobuilding coq-lsp is necessary
(not that coq-lsp has to address all cases necessarily)
Autobuild deals with that in the same way that other build systems in Coq do
The goal with coq-lsp is not to care too much about files
In that sense, there should be no difference from building a file and building just a single proof in that file
?
I mean, if coq-lsp is for 8.17 but my code is for 8.16, how does auto-build help?
It doesn't
Note that .vo files are versioned in way finer ways than Coq versions
for example they don't work across different ocaml versions (including minor ones)
and a lot of other stuff
so users find this problem very often
Okay, auto-build will help with that
Yup, auto-build only deals with the build part, it would be interesting to think a bit more about packaging too yes
(IME just rebuilding the same source can trigger mismatches, maybe because of non-reproducibility)
Yes that can indeed happen
But as Andrey Mokhov put it, the idea is to explore the combination of build system with compiler
What I meant above about coq-lsp not caring too much about files is that indeed, for Flèche you just tell the system what you need
So files are just another kind of object in the dep graph
For example something I hope to get to the main branch soon is the capability of Require
not having to build the full file
tho indeed in this case we still trade soundness for speed due to univ constraints
however you can still have some hope of incrementality, in the sense than when proofs are checked, if no new univ constraints are produced, you won't redo work
It will be interesting to see how the dep data behaves
See for example https://github.com/ejgallego/coq-lsp/issues/310
Vos/vok has similar questions and people pointed out worse problems (ltac in one proof can backtrack because of constraints from a different proof), tho if anything I'd try changing the semantics of "normal" builds to be more compositional: instead of "fixing the behavior of vos builds", I'd try to treat the normal "vo" builds as buggy, and move all consistency checking to "link-time"
I'm afraid I don't understand what you propose, can you provide an example of such "link-time" checking?
It is fine for coq-lsp / Flèche that checking a proof may impact everything, having a good UI / heuristics to decide when the tradeoff is worth it is the main open problem IMHO.
Emilio Jesús Gallego Arias said:
The right solution to this problem --- which I'm hoping to implement soon --- is to have coq-lsp support auto-build of .vo files, so you never ever have this problem again as coq-lsp will detect a .vo is not right and re-build it on the fly.
Meanwhile, you have the following options:
- use
main
branch and "vendor" your Coq libraries too, that is to say, place the sources invendor/my_coq_lib
and usedune exec -- make
ordune exec -- coqc
etc... to build them- use
main
branch but use an opam switch: in this case you'll need to pin Coq (and coq-serapi) to coq.dev from the Coq Opam repository, and remove thevendor
directory.- use
v8.17
and opam (and be sure that git removes thevendor
directory).
so if i vendor my libraries and use main it actually yells at me about a dependency cycle when i try to make lsp:
Dependency cycle between:
Computing installable artifacts for package coqide-server
-> required by Computing installable artifacts for package coq-core
-> required by _build/default/vendor/coq/coq-core.install
that claims coq-core
depends on coqide-server
it only comes up when i copy my libraries over though? and none of them use coqide-server
nvm fixed it
nope, still bad version number errors which means it seems to have compiled with 8.17.0?
I guess the vendoring didn't work?
Please open a bug and I'll update the contributing guide to explain how to do this very important use case.
I'll have to wait for Thu tho, tomorrow I'm all day locked in a workshop + PhD defense
For now I'd suggest you just use the 8.17 branch then
be sure the vendor
dir has gone away
will create an issue this weekend! been quite busy all week but def not forgetting this.
I'm just curious @Emilio Jesús Gallego Arias -- what's the motivation behind using a vendored version? It seems to me a lot of projects are in a state of "only compiles on coq 8.x" and this seems to prevent them from using lsp as the dependencies won't load at all
Having a vendored copy allows you to develop Coq at the same time. It isn't entirely necessary anymore and remove them, but we just haven't gotten round to doing it yet.
@Bhakti Shah what are those projects (out of curiosity) ?
We have the versioned branches that don't require versioning, actually you can indeed remove vendoring and use Coq's opam package for Coq master, and it would work.
But unfortunately Coq's API is not compatible among versions, so we need to have a branch for each Coq release, and backport. I don't see any other way to handle older Coq projects.
Ideally Coq API would be in a better state to the point something like coq-lsp could be developed versus a stable Coq version (like 8.17), and in fact, to avoid the problems that developing against master imply I did proposed to work on the API first in 2019, but not a lot of progress happened so far (we have barely got the minimum amount of API to be able to write a basic client without hacks, but far from what more advanced features do need)
We will however as I said work on a better solution for coq-lsp development based on coq-universe soon.
So it’s these projects [https://github.com/inQWIRE/QuantumLib, https://github.com/inQWIRE/SQIR, https://github.com/inQWIRE/VyZX]
I think the changes that I made to coq-lsp aren’t part of any of the released versions (and I tried pinning to different branches but I’m not sure if the opam file needed updating); either way I think working in the extension dev host was the only thing that worked for me as my changes aren’t a part of the branches that don’t have vendoring
Last updated: Apr 18 2024 at 07:02 UTC