Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Internal assertion error from "library/lib.ml" #943

Open
westpaddy opened this issue Nov 8, 2024 · 0 comments
Open

Internal assertion error from "library/lib.ml" #943

westpaddy opened this issue Nov 8, 2024 · 0 comments

Comments

@westpaddy
Copy link

westpaddy commented Nov 8, 2024

Editing or viewing .v files in this (ConCert) project, I sometimes get the following error.
スクリーンショット 2024-11-08 18 35 44
After the error, vscoq becomes unstable, resulting in most of the functionality does not work.
(looks like https://github.com/coq/coq/blob/V8.18.0/library/lib.ml#L456)

This seems the same issue found at the this zulip-archive.

Reproduction steps

I'm afraid I cannot find a small error reproduction process.
The following is the instruction for reproducing the error using the ConCert project.

Suppose vscoq is installed on vscode.
Run the following command to build the project and open a vscode workspace.

git clone https://github.com/AU-COBRA/ConCert.git
cd ConCert
opam switch create . 4.14.2 --repositories default,coq-released=https://coq.inria.fr/opam/released --deps-only
eval $(opam env)
make
opam install vscoq-language-server
cd execution
code .

Now open multiple files, for example, theories/Blockchain.v and theories/BoundedN.v.
We will get the error message.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant