VsCoq Legacy not working with rocq dev + compat layer?

[mattam82]

I get this when trying to run VsCoq 1 on a fresh Rocq master install + the coq compatibility packages:

# opam list | grep "\(coq\|rocq\)"
coq                     dev         pinned to version dev at git+https://github.com/coq/coq.git#master
coq-core                dev         pinned to version dev at git+https://github.com/coq/coq.git#master
coq-equations           dev         A function definition package for Coq
coq-stdlib              dev         Compatibility metapackage for Coq Stdlib library after the Rocq renaming
coqide-server           dev         pinned to version dev at git+https://github.com/coq/coq.git#master
rocq-core               dev         pinned to version dev at git+https://github.com/coq/coq.git#master
rocq-prover             dev         pinned to version dev at git+https://github.com/coq/coq.git#master
rocq-runtime            dev         pinned to version dev at git+https://github.com/coq/coq.git#master
rocq-stdlib             dev         The Rocq Proof Assistant -- Standard Library
rocqide                 dev         pinned to version dev at git+https://github.com/coq/coq.git#master

starting coqtop
exec: _opam/bin/coqtop -v
Listening at 127.0.0.1:64296
Listening at 127.0.0.1:64297
Listening at 127.0.0.1:64298
Listening at 127.0.0.1:64299
[Warn  - 10:32:51] Could not detect coqtop version, defaulting to >= 8.10.
Coqtop version parsed into semver version 8.10.0
exec: _opam/bin/coqidetop -main-channel 127.0.0.1:64296:64298 -control-channel 127.0.0.1:64297:64299 -async-proofs on -R utils/theories MetaCoq.Utils -R common/theories MetaCoq.Common -R template-coq/theories MetaCoq.Template -I template-coq -I template-coq/src -R pcuic/theories MetaCoq.PCUIC -I pcuic -I pcuic/src -R template-pcuic/theories MetaCoq.TemplatePCUIC -R safechecker/theories MetaCoq.SafeChecker -R safechecker-plugin/theories MetaCoq.SafeCheckerPlugin -I safechecker-plugin -I safechecker-plugin/src -R erasure/theories MetaCoq.Erasure -R erasure-plugin/theories MetaCoq.ErasurePlugin -I erasure-plugin -I erasure-plugin/src -R translations MetaCoq.Translations -R quotation/theories MetaCoq.Quotation -R test-suite MetaCoq.TestSuite -R test-suite/plugin-demo/theories MetaCoq.ExtractedPluginDemo -I test-suite/plugin-demo -I test-suite/plugin-demo/src -R examples MetaCoq.Examples -topfile /Volumes/Data/dev/coq/MetaCoq-main/test-suite/erasure_live_test.v
coqtop started with pid 57918
Client connected on main channel R (port 64296)
Client connected on main channel W (port 64298)
Client connected on control channel R (port 64297)
Client connected on control channel W (port 64299)
--------------------------------
Call Init()
Init: () --> 1
--------------------------------
Call Add("From Stdlib Require ...", editId: 0, stateId: 1, verbose: false)
coqtop-stderr: [pid 57918] Unexpected XML message
[pid 57918] Expected XML node: int
[pid 57918] XML tree received: <bool val="false"/>

Any idea what might be wrong?

[SkySkimmer]

IT looks for "the coq proof assistant" to detect version https://github.com/coq-community/vscoq-legacy/blob/cae8345ee25468fca16f08f0b8da2965ead75424/server/src/coqtop/CoqTop.ts#L105
and there's at least one difference between the fallback 8.10 and current https://github.com/coq-community/vscoq-legacy/blob/cae8345ee25468fca16f08f0b8da2965ead75424/server/src/coqtop/IdeSlave8.ts#L320

[SkySkimmer]

PS vscoq legacy issues are at https://github.com/coq-community/vscoq-legacy/issues not here

[thery]

@mattam82 I guess it is because if the new name. I think VsCoq Legacy expects the line "The Coq Proof Assistant, version ..." to get the version numer. Try to see if coqtop -v outputs "The Coq Prover, version 9.0" instead of
"The Rocq Prover, version 9.0" it works any better.

[gares]

Yes this issue is out of place. @thery if you can fix the regexp and make a release of legacy, that would be nice ;-)

[thery]

@gares Ok I will try

[thery]

@mattam82 I have just published VsCoq Legacy version 0.5.0. Can you try it to check if it works?

Ps: As it is a legacy stuff, you need to have the coq package (i.e. coqtop and coqidetop need to be available on your machine)