bad version number errors · coq-lsp

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.

Paolo Giarrusso (Apr 16 2023 at 10:27):

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)

Paolo Giarrusso (Apr 16 2023 at 11:28):

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

Bhakti Shah (Apr 16 2023 at 17:07):

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?

Bhakti Shah (Apr 16 2023 at 17:09):

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

Paolo Giarrusso (Apr 17 2023 at 00:48):

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.

Paolo Giarrusso (Apr 17 2023 at 00:48):

Bhakti Shah (Apr 17 2023 at 04:37):

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

Bhakti Shah (Apr 17 2023 at 04:39):

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

Paolo Giarrusso (Apr 17 2023 at 05:41):

Paolo Giarrusso (Apr 17 2023 at 05:53):

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?

Paolo Giarrusso (Apr 17 2023 at 06:01):

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

Bhakti Shah (Apr 17 2023 at 07:43):

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.

Emilio Jesús Gallego Arias (Apr 18 2023 at 14:06):

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.

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

Emilio Jesús Gallego Arias (Apr 18 2023 at 14:06):

However if you have an opam setup with files in .opam/foo/lib/coq/user-contrib/Uuuuh.vo

Emilio Jesús Gallego Arias (Apr 18 2023 at 14:07):

Emilio Jesús Gallego Arias (Apr 18 2023 at 14:10):

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.

Alex Sanchez-Stern (Apr 18 2023 at 16:48):

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.

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:12):

Yes, indeed coq-lsp will maintain its own binary cache, so that shouldn't be a problem

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:13):

Sound caching goes beyond keeping track of Coq versions, you also need to keep track of .v file versions, etc...

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:15):

But certainly it is a priority that coq-lsp users never see again that mismatch problem.

Paolo Giarrusso (Apr 18 2023 at 17:24):

Paolo Giarrusso (Apr 18 2023 at 17:26):

Autobuilding sources is good for other reasons, but for version mismatches it seems autobuilding coq-lsp is necessary

Paolo Giarrusso (Apr 18 2023 at 17:27):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:27):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:28):

In that sense, there should be no difference from building a file and building just a single proof in that file

Paolo Giarrusso (Apr 18 2023 at 17:28):

Paolo Giarrusso (Apr 18 2023 at 17:29):

I mean, if coq-lsp is for 8.17 but my code is for 8.16, how does auto-build help?

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:29):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:30):

for example they don't work across different ocaml versions (including minor ones)

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:30):

Paolo Giarrusso (Apr 18 2023 at 17:30):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:31):

Yup, auto-build only deals with the build part, it would be interesting to think a bit more about packaging too yes

Paolo Giarrusso (Apr 18 2023 at 17:32):

(IME just rebuilding the same source can trigger mismatches, maybe because of non-reproducibility)

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:32):

But as Andrey Mokhov put it, the idea is to explore the combination of build system with compiler

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:33):

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

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:34):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:36):

For example something I hope to get to the main branch soon is the capability of Require not having to build the full file

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:36):

tho indeed in this case we still trade soundness for speed due to univ constraints

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:37):

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

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:38):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:39):

Paolo Giarrusso (Apr 18 2023 at 17:46):

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"

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:58):

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.

Bhakti Shah (Apr 18 2023 at 20:42):

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

Paolo Giarrusso (Apr 18 2023 at 20:46):

Bhakti Shah (Apr 18 2023 at 21:22):

it only comes up when i copy my libraries over though? and none of them use coqide-server

Bhakti Shah (Apr 18 2023 at 21:42):

Bhakti Shah (Apr 18 2023 at 22:25):

nope, still bad version number errors which means it seems to have compiled with 8.17.0?

Emilio Jesús Gallego Arias (Apr 18 2023 at 22:41):

Please open a bug and I'll update the contributing guide to explain how to do this very important use case.

Emilio Jesús Gallego Arias (Apr 18 2023 at 22:41):

I'll have to wait for Thu tho, tomorrow I'm all day locked in a workshop + PhD defense

Emilio Jesús Gallego Arias (Apr 18 2023 at 22:41):

Bhakti Shah (Apr 21 2023 at 01:18):

will create an issue this weekend! been quite busy all week but def not forgetting this.

Bhakti Shah (Apr 27 2023 at 06:40):

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

Ali Caglayan (Apr 27 2023 at 16:19):

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.

Emilio Jesús Gallego Arias (Jun 06 2023 at 19:20):

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.

Bhakti Shah (Jun 08 2023 at 20:42):

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

Stream: coq-lsp

Topic: bad version number errors

Bhakti Shah (Apr 16 2023 at 03:28):

Paolo Giarrusso (Apr 16 2023 at 10:27):

Paolo Giarrusso (Apr 16 2023 at 11:28):

Bhakti Shah (Apr 16 2023 at 17:07):

Bhakti Shah (Apr 16 2023 at 17:09):

Paolo Giarrusso (Apr 17 2023 at 00:48):

Paolo Giarrusso (Apr 17 2023 at 00:48):

Bhakti Shah (Apr 17 2023 at 04:37):

Bhakti Shah (Apr 17 2023 at 04:39):

Paolo Giarrusso (Apr 17 2023 at 05:41):

Paolo Giarrusso (Apr 17 2023 at 05:53):

Paolo Giarrusso (Apr 17 2023 at 06:01):

Bhakti Shah (Apr 17 2023 at 07:43):

Emilio Jesús Gallego Arias (Apr 18 2023 at 14:06):

Emilio Jesús Gallego Arias (Apr 18 2023 at 14:06):

Emilio Jesús Gallego Arias (Apr 18 2023 at 14:07):

Emilio Jesús Gallego Arias (Apr 18 2023 at 14:10):

Alex Sanchez-Stern (Apr 18 2023 at 16:48):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:12):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:13):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:15):

Paolo Giarrusso (Apr 18 2023 at 17:24):

Paolo Giarrusso (Apr 18 2023 at 17:26):

Paolo Giarrusso (Apr 18 2023 at 17:27):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:27):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:28):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:28):

Paolo Giarrusso (Apr 18 2023 at 17:28):

Paolo Giarrusso (Apr 18 2023 at 17:29):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:29):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:29):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:30):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:30):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:30):

Paolo Giarrusso (Apr 18 2023 at 17:30):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:31):

Paolo Giarrusso (Apr 18 2023 at 17:32):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:32):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:32):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:33):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:34):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:36):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:36):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:37):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:38):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:39):

Paolo Giarrusso (Apr 18 2023 at 17:46):

Emilio Jesús Gallego Arias (Apr 18 2023 at 17:58):

Bhakti Shah (Apr 18 2023 at 20:42):

Paolo Giarrusso (Apr 18 2023 at 20:46):

Bhakti Shah (Apr 18 2023 at 21:22):

Bhakti Shah (Apr 18 2023 at 21:42):

Bhakti Shah (Apr 18 2023 at 22:25):

Emilio Jesús Gallego Arias (Apr 18 2023 at 22:41):

Emilio Jesús Gallego Arias (Apr 18 2023 at 22:41):

Emilio Jesús Gallego Arias (Apr 18 2023 at 22:41):

Emilio Jesús Gallego Arias (Apr 18 2023 at 22:41):

Bhakti Shah (Apr 21 2023 at 01:18):

Bhakti Shah (Apr 27 2023 at 06:40):

Ali Caglayan (Apr 27 2023 at 16:19):

Emilio Jesús Gallego Arias (Jun 06 2023 at 19:20):

Bhakti Shah (Jun 08 2023 at 20:42):