ergo icon indicating copy to clipboard operation
ergo copied to clipboard

Cannot build from sources due to incompatible coq-jsast.3.0.0

Open prekel opened this issue 1 year ago • 0 comments

Bug Report 🐛

I trying to build project following the instruction from DEVELOPERS.md

Current Behavior

#=== ERROR while compiling coq-qcert.2.1.1 ====================================#
# context     2.1.2 | linux/x86_64 | ocaml-base-compiler.4.11.2 | https://coq.inria.fr/opam/released#2022-07-04 11:30
# path        ~/.opam/ergo/.opam-switch/build/coq-qcert.2.1.1
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j 11 coq-qcert
# exit-code   2
# env-file    ~/.opam/log/coq-qcert-29393-24894d.env
# output-file ~/.opam/log/coq-qcert-29393-24894d.out
### output ###
# [...]
# COQC compiler/core/Translation/Lang/JavaScriptAsttoJavaScript.v
# File "./compiler/core/Translation/Lang/JavaScriptAsttoJavaScript.v", line 64, characters 2-295:
# Error: Non exhaustive pattern-matching: no clause found for pattern
# literal_bigint _
# 
# make[3]: *** [Makefile.coq:715: compiler/core/Translation/Lang/JavaScriptAsttoJavaScript.vo] Error 1
# make[3]: *** Waiting for unfinished jobs....
# make[2]: *** [Makefile.coq:339: all] Error 2
# make[2]: Leaving directory '/home/vladislav/.opam/ergo/.opam-switch/build/coq-qcert.2.1.1'
# make[1]: *** [Makefile:147: qcert-coq] Error 2
# make[1]: Leaving directory '/home/vladislav/.opam/ergo/.opam-switch/build/coq-qcert.2.1.1'
# make: *** [Makefile:78: coq-qcert] Error 2

Possible Solution

Explicitly install previous version of coq-jsast:

opam install coq.8.12.2 coq-qcert.2.1.1 coq-jsast.2.0.0

Context (Environment)

Desktop

  • OS: WSL Ubuntu 20.04

prekel avatar Jul 05 '22 03:07 prekel