Address errors on opening/loading .v files #93

New issue

Open

opened 2026-10-29 14:56:52 +01:00 by marfavi · 0 comments

marfavi commented

2026-10-29 14:56:52 +01:00

Owner

Opening v files can result in VsRocq errors like:

cannot add object (REQUIRE-SYNTAX, in synterp): not initialized(quickfix-replace) as a diagnostic on the first line
error message notification with Error while opening document. The global environment cannot be accessed during the syntactic interpretation phase.
error message notification with Error while opening document. Anomaly "File "kernel/safe_typing.ml", line 1472, characters 2-8: Assertion failed." Please report at http://rocq-prover.org/bugs/.

(Find reproducible example...)

Opening v files can result in VsRocq errors like: * `cannot add object (REQUIRE-SYNTAX, in synterp): not initialized(quickfix-replace)` as a diagnostic on the first line * error message notification with `Error while opening document. The global environment cannot be accessed during the syntactic interpretation phase.` * error message notification with `Error while opening document. Anomaly "File "kernel/safe_typing.ml", line 1472, characters 2-8: Assertion failed." Please report at http://rocq-prover.org/bugs/.` (Find reproducible example...)

marfavi added the

priority!

label

2026-10-29 14:56:58 +01:00

marfavi added this to the Release roadmap project

2026-10-29 15:34:58 +01:00