Skip to content
This repository was archived by the owner on Sep 7, 2023. It is now read-only.
This repository was archived by the owner on Sep 7, 2023. It is now read-only.

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

@prekel

Description

@prekel

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions