Stream: math-comp users

Topic: Problem installing odd-order with opam

view this post on Zulip Assia Mahboubi (Oct 18 2023 at 16:37):

Hello, here is what is get when trying to install the odd order opam package:

amahboub@alebrije:~$ opam install coq-mathcomp-odd-order
The following actions will be performed:
   install coq-mathcomp-odd-order 1.14.0

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
 retrieved coq-mathcomp-odd-order.1.14.0  (cached)
[ERROR] The compilation of coq-mathcomp-odd-order.1.14.0 failed at "make -j 15".

#=== ERROR while compiling coq-mathcomp-odd-order.1.14.0 ======================#
# context     2.1.2 | linux/x86_64 | ocaml-base-compiler.4.12.1 | 13:18
# path        ~/.opam/with-coq/.opam-switch/build/coq-mathcomp-odd-order.1.14.0
# command     ~/.opam/opam-init/hooks/ build make -j 15
# exit-code   2
# env-file    ~/.opam/log/coq-mathcomp-odd-order-383749-02aa79.env
# output-file ~/.opam/log/coq-mathcomp-odd-order-383749-02aa79.out
### output ###
# [...]
# Use rmorphXn instead.
# [deprecated-syntactic-definition-since-mathcomp-1.17.0,deprecated-since-mathcomp-1.17.0,deprecated-syntactic-definition,deprecated,default]
# File "./theories/PFsection1.v", line 617, characters 7-68:
# Error: The LHS of chinese_modl
#     (chinese _ _ _ _ %% _)
# does not match any subterm of the goal
# make[2]: *** [Makefile.coq:838 : theories/PFsection1.vo] Erreur 1
# make[2]: *** [theories/PFsection1.vo] Suppression du fichier « theories/PFsection1.glob »
# make[2]: *** Attente des tâches non terminées....
# make[1]: *** [Makefile.coq:409 : all] Erreur 2
# make: *** [Makefile:15 : invoke-coqmakefile] Erreur 2

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
 λ build coq-mathcomp-odd-order 1.14.0
╶─ No changes have been performed

view this post on Zulip Assia Mahboubi (Oct 18 2023 at 16:37):

Note that I first had to manually upgrade mathcomp packages to version 2.0.

view this post on Zulip Assia Mahboubi (Oct 18 2023 at 16:38):

Here is my opam list:

view this post on Zulip Assia Mahboubi (Oct 18 2023 at 16:38):

# Packages matching: installed
# Name                      # Installed    # Synopsis
astring                     0.8.5          Alternative String module for OCaml
atd                         2.13.0         Parser for the ATD data format description language
atdgen                      2.13.0         Generates efficient JSON serializers, deserializers
atdgen-runtime              2.13.0         Runtime library for code generated by atdgen
atdts                       2.13.0         TypeScript code generation for ATD APIs
base-bigarray               base
base-threads                base
base-unix                   base
biniou                      1.2.2          Binary data format designed for speed, safety, ease
bos                         0.2.1          Basic OS interaction for OCaml
camlp-streams               5.0.1          The Stream and Genlex libraries for use with Camlp4
camlp5                      8.02.00        Preprocessor-pretty-printer of OCaml
camlp5-buildscripts         0.03           Camlp5 Build scripts (written in OCaml)
cmdliner                    1.2.0          Declarative definition of command line interfaces fo
conf-bash                   1              Virtual package to install the Bash shell
conf-findutils              1              Virtual package relying on findutils
conf-g++                    1.0            Virtual package relying on the g++ compiler (for C++
conf-gmp                    4              Virtual package relying on a GMP lib system installa
conf-libpcre                1              Virtual package relying on a libpcre system installa
conf-m4                     1              Virtual package relying on m4
conf-perl                   2              Virtual package relying on perl
conf-perl-ipc-system-simple 3              Virtual package relying on perl's IPC::System::Simpl
conf-perl-string-shellquote 3              Virtual package relying on perl's String::ShellQuote
conf-pkg-config             3              Check if pkg-config is installed and create an opam
conf-which                  1              Virtual package relying on which
coq                         8.18.0         The Coq Proof Assistant
coq-autosubst               1.8            Coq library for parallel de Bruijn substitutions
coq-bignums                 9.0.0+coq8.18  Bignums, the Coq library of arbitrarily large number
coq-coquelicot              3.4.0          A Coq formalization of real analysis compatible with
coq-core                    8.18.0         The Coq Proof Assistant -- Core Binaries and Tools
coq-elpi                    1.19.3         Elpi extension language for Coq
coq-equations               1.3+8.18       A function definition package for Coq
coq-flocq                   4.1.3          A formalization of floating-point arithmetic for the
coq-hierarchy-builder       1.6.0          High level commands to declare and evolve a hierarch
coq-interval                4.8.1          A Coq tactic for proving bounds on real-valued expre
coq-itauto                  8.18.0         Reflexive SAT solver with Nelson-Oppen support, para
coq-mathcomp-algebra        2.0.0          Mathematical Components Library on Algebra
coq-mathcomp-character      2.0.0          Mathematical Components Library on character theory
coq-mathcomp-field          2.0.0          Mathematical Components Library on Fields
coq-mathcomp-fingroup       2.0.0          Mathematical Components Library on finite groups
coq-mathcomp-solvable       2.0.0          Mathematical Components Library on finite groups (II
coq-mathcomp-ssreflect      2.0.0          Small Scale Reflection
coq-mathcomp-zify           1.5.0+2.0+8.16 Micromega tactics for Mathematical Components
coq-stdlib                  8.18.0         The Coq Proof Assistant -- Standard Library
coqide-server               8.18.0         The Coq Proof Assistant, XML protocol server
cppo                        1.6.9          Code preprocessor like cpp for OCaml
csexp                       1.5.2          Parsing and printing of S-expressions in Canonical f
dune                        3.10.0         Fast, portable, and opinionated build system
dune-configurator           3.10.0         Helper library for gathering system configuration
easy-format                 1.3.4          High-level and functional interface to the Format mo
elpi                        1.17.4         ELPI - Embeddable λProlog Interpreter
fmt                         0.9.0          OCaml Format pretty-printer combinators
fpath                       0.7.3          File system paths for OCaml
logs                        0.7.0          Logging infrastructure for OCaml
menhir                      20230608       An LR(1) parser generator
menhirLib                   20230608       Runtime support library for parsers generated by Men
menhirSdk                   20230608       Compile-time library for auxiliary tools related to
not-ocamlfind               0.10           A small frontend for ocamlfind that adds a few usefu
ocaml                       4.12.1         The OCaml compiler (virtual package)
ocaml-base-compiler         4.12.1         Official release 4.12.1
ocaml-compiler-libs         v0.12.4        OCaml compiler libraries repackaged
ocaml-config                2              OCaml Switch Configuration
ocaml-options-vanilla       1              Ensure that OCaml is compiled with no special option
ocaml-secondary-compiler    4.08.1-1       OCaml 4.08.1 Secondary Switch Compiler
ocamlbuild                  0.14.2         OCamlbuild is a build system with builtin rules to e
ocamlfind                   1.9.6          A library manager for OCaml
ocamlfind-secondary         1.9.6          Adds support for ocaml-secondary-compiler to ocamlfi
ocamlgraph                  2.0.0          A generic graph library for OCaml
pcre                        7.5.0          Bindings to the Perl Compatibility Regular Expressio
ppx_derivers                1.2.1          Shared [@@deriving] plugin registry
ppx_deriving                5.2.1          Type-driven code generation for OCaml
ppxlib                      0.30.0         Standard infrastructure for ppx rewriters
re                          1.11.0         RE is a regular expression library for OCaml
result                      1.5            Compatibility Result module
rresult                     0.7.0          Result value combinators for OCaml
seq                         base           Compatibility package for OCaml's standard iterator
sexplib0                    v0.16.0        Library containing the definition of S-expressions a
stdlib-shims                0.3.0          Backport some of the new stdlib features to older co
topkg                       1.0.7          The transitory OCaml software packager
yojson                      2.1.1          Yojson is an optimized parsing and printing library
zarith                      1.13           Implements arithmetic and logical operations over ar

view this post on Zulip Karl Palmskog (Oct 18 2023 at 16:45):

the problem is that the package coq-mathcomp-odd-order.1.14.0 inaccurately does not specify an upper bound on the MathComp version, it just has >= 1.12. I will add an upper bound in the Coq opam archive

view this post on Zulip Karl Palmskog (Oct 18 2023 at 17:03):

view this post on Zulip Pierre Roux (Oct 18 2023 at 17:08):

Apparently, the MC 2.0 branch was merged but never released, here it is:

Last updated: Jul 15 2024 at 21:02 UTC