Created
December 20, 2024 12:27
-
-
Save SkySkimmer/1781b418899354ded0a41ab668b167a4 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| The following actions will be performed: | |
| ∗ install coq-rewriter-perf-SuperFast dev | |
| <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> | |
| Processing 1/3: [coq-rewriter-perf-SuperFast.dev: git] | |
| ⬇ retrieved coq-rewriter-perf-SuperFast.dev (git+https://github.com/mit-plv/rewriter.git#master) | |
| Processing 2/3: [coq-rewriter-perf-SuperFast: make perf-SuperFast] | |
| + /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/dev/bench/wrapper.sh "make" "-j1" "perf-SuperFast" "EXTERNAL_PERF_DEPENDENCIES=1" "TIMED=1" (CWD=/home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-rewriter-perf-SuperFast.dev) | |
| - sed 's?@META@?src/Rewriter/Util/plugins/META.coq-rewriter?g' _CoqProject.in > _CoqProject | |
| - echo $COQ_VERSION_INFO (9.0+alpha) > .coq-version | |
| - COQ_MAKEFILE -f _CoqProject > Makefile.coq | |
| - Warning: native compilation is globally deactivated by the configure flag | |
| - COQ_MAKEFILE -f _CoqProject > Makefile.coq | |
| - Warning: native compilation is globally deactivated by the configure flag | |
| - CP src/Rewriter/Util/Tactics2/Constr.v{.v821,} | |
| - CP src/Rewriter/Util/Tactics2/DestCase.v{.v821,} | |
| - CP src/Rewriter/Util/Tactics2/DestProj.v{.v821,} | |
| - CP src/Rewriter/Util/Tactics2/Proj.v{.v821,} | |
| - CP src/Rewriter/Util/plugins/RewriterBuildRegistry.v{.v821,} | |
| - CP src/Rewriter/Util/plugins/RewriterBuild.v{.v821,} | |
| - CP src/Rewriter/Util/plugins/StrategyTactic.v{.v821,} | |
| - CP src/Rewriter/Util/plugins/Ltac2Extra.v{.v821,} | |
| - CP src/Rewriter/Util/plugins/definition_by_tactic.ml{.v821,} | |
| - CP src/Rewriter/Util/plugins/definition_by_tactic.mli{.v821,} | |
| - CP src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg{.v821,} | |
| - CP src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib{.v821,} | |
| - CP src/Rewriter/Util/plugins/inductive_from_elim.ml{.v821,} | |
| - CP src/Rewriter/Util/plugins/inductive_from_elim.mli{.v821,} | |
| - CP src/Rewriter/Util/plugins/inductive_from_elim_plugin.mlg{.v821,} | |
| - CP src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib{.v821,} | |
| - CP src/Rewriter/Util/plugins/rewriter_build.ml{.v821,} | |
| - CP src/Rewriter/Util/plugins/rewriter_build.mli{.v821,} | |
| - CP src/Rewriter/Util/plugins/rewriter_build_plugin.mlg{.v821,} | |
| - CP src/Rewriter/Util/plugins/rewriter_build_plugin.mllib{.v821,} | |
| - CP src/Rewriter/Util/plugins/strategy_tactic.ml{.v821,} | |
| - CP src/Rewriter/Util/plugins/strategy_tactic.mli{.v821,} | |
| - CP src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg{.v821,} | |
| - CP src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib{.v821,} | |
| - CP src/Rewriter/Util/plugins/ltac2_extra.ml{.v821,} | |
| - CP src/Rewriter/Util/plugins/ltac2_extra.mli{.v821,} | |
| - CP src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg{.v821,} | |
| - CP src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib{.v821,} | |
| - ROCQ DEP VFILES | |
| - COQPP src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg | |
| - COQPP src/Rewriter/Util/plugins/inductive_from_elim_plugin.mlg | |
| - COQPP src/Rewriter/Util/plugins/rewriter_build_plugin.mlg | |
| - COQPP src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg | |
| - COQPP src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg | |
| - CAMLDEP src/Rewriter/Util/plugins/ltac2_extra.mli | |
| - CAMLDEP src/Rewriter/Util/plugins/strategy_tactic.mli | |
| - CAMLDEP src/Rewriter/Util/plugins/rewriter_build.mli | |
| - CAMLDEP src/Rewriter/Util/plugins/inductive_from_elim.mli | |
| - CAMLDEP src/Rewriter/Util/plugins/definition_by_tactic.mli | |
| - OCAMLLIBDEP src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib | |
| - OCAMLLIBDEP src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib | |
| - OCAMLLIBDEP src/Rewriter/Util/plugins/rewriter_build_plugin.mllib | |
| - OCAMLLIBDEP src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib | |
| - OCAMLLIBDEP src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib | |
| - CAMLDEP src/Rewriter/Util/plugins/ltac2_extra.ml | |
| - CAMLDEP src/Rewriter/Util/plugins/strategy_tactic.ml | |
| - CAMLDEP src/Rewriter/Util/plugins/rewriter_build.ml | |
| - CAMLDEP src/Rewriter/Util/plugins/inductive_from_elim.ml | |
| - CAMLDEP src/Rewriter/Util/plugins/definition_by_tactic.ml | |
| - CAMLDEP src/Rewriter/Util/plugins/ltac2_extra_plugin.ml | |
| - CAMLDEP src/Rewriter/Util/plugins/strategy_tactic_plugin.ml | |
| - CAMLDEP src/Rewriter/Util/plugins/rewriter_build_plugin.ml | |
| - CAMLDEP src/Rewriter/Util/plugins/inductive_from_elim_plugin.ml | |
| - CAMLDEP src/Rewriter/Util/plugins/definition_by_tactic_plugin.ml | |
| - SED Template.v.in > LiftLetsMap/_0_SuperFast.v | |
| - ROCQ compile src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v", line 1, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v", line 2, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v", line 3, characters 0-28: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v", line 4, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v", line 5, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v", line 6, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Harness.v", line 7, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Rewriter/Examples/PerfTesting/Harness.vo (real: 0.98, user: 0.83, sys: 0.14, mem: 428080 ko) | |
| - ROCQ compile src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v", line 1, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v", line 2, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.v", line 3, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.vo (real: 0.21, user: 0.13, sys: 0.07, mem: 158764 ko) | |
| - ROCQ compile src/Rewriter/Util/GlobalSettings.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/GlobalSettings.vo (real: 0.14, user: 0.05, sys: 0.09, mem: 95128 ko) | |
| - ROCQ compile src/Rewriter/Util/FixCoqMistakes.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/FixCoqMistakes.v", line 2, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/FixCoqMistakes.v", line 33, characters 5-34: | |
| - Warning: Coq.Init.Tactics.assert_fails has been replaced by | |
| - Corelib.Init.Tactics.assert_fails. | |
| - [deprecated-dirpath-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Util/FixCoqMistakes.vo (real: 0.16, user: 0.08, sys: 0.08, mem: 117612 ko) | |
| - ROCQ compile src/Rewriter/Util/Notations.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 34, characters 0-72: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 35, characters 0-59: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 36, characters 0-52: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 36, characters 0-52: | |
| - Warning: Notations "_ + _" defined at level 50 with arguments constr | |
| - at level 50 and "_ +" defined at level 50 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 37, characters 0-52: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 37, characters 0-52: | |
| - Warning: Notations "_ * _" defined at level 40 with arguments constr | |
| - at level 40 and "_ *" defined at level 40 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 57, characters 0-56: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 58, characters 0-56: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 111, characters 0-36: | |
| - Warning: Closed notations (i.e. starting and ending with a terminal symbol) | |
| - should usually be at level 0 (default). | |
| - [closed-notation-not-level-0,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 112, characters 0-36: | |
| - Warning: Closed notations (i.e. starting and ending with a terminal symbol) | |
| - should usually be at level 0 (default). | |
| - [closed-notation-not-level-0,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 113, characters 0-37: | |
| - Warning: Closed notations (i.e. starting and ending with a terminal symbol) | |
| - should usually be at level 0 (default). | |
| - [closed-notation-not-level-0,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 114, characters 0-37: | |
| - Warning: Closed notations (i.e. starting and ending with a terminal symbol) | |
| - should usually be at level 0 (default). | |
| - [closed-notation-not-level-0,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 115, characters 0-38: | |
| - Warning: Closed notations (i.e. starting and ending with a terminal symbol) | |
| - should usually be at level 0 (default). | |
| - [closed-notation-not-level-0,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 116, characters 0-38: | |
| - Warning: Closed notations (i.e. starting and ending with a terminal symbol) | |
| - should usually be at level 0 (default). | |
| - [closed-notation-not-level-0,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 130, characters 0-42: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 130, characters 0-42: | |
| - Warning: Notations "_ [ ? ]" defined at level 9 with arguments constr | |
| - at next level and "_ [ _ ]" defined at level 30 with arguments constr | |
| - at next level have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 131, characters 0-44: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 132, characters 0-44: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 146, characters 0-151: | |
| - Warning: Notations "slet _ .. _ <- _ ; _" defined at level 70 with arguments | |
| - binder and "slet _ .. _ := _ in _" defined at level 200 with arguments binder | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 166, characters 0-129: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 174, characters 0-248: | |
| - Warning: Closed notations (i.e. starting and ending with a terminal symbol) | |
| - should usually be at level 0 (default). | |
| - [closed-notation-not-level-0,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 176, characters 0-334: | |
| - Warning: Closed notations (i.e. starting and ending with a terminal symbol) | |
| - should usually be at level 0 (default). | |
| - [closed-notation-not-level-0,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 180, characters 0-54: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 181, characters 0-54: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - File "./src/Rewriter/Util/Notations.v", line 186, characters 0-61: | |
| - Warning: Postfix notations (i.e. starting with a nonterminal symbol and | |
| - ending with a terminal symbol) should usually be at level 1 (default). | |
| - [postfix-notation-not-level-1,parsing,default] | |
| - src/Rewriter/Util/Notations.vo (real: 0.18, user: 0.09, sys: 0.08, mem: 143652 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/GetGoal.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/GetGoal.vo (real: 0.14, user: 0.07, sys: 0.07, mem: 95716 ko) | |
| - ROCQ compile src/Rewriter/Util/LetIn.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/LetIn.v", line 2, characters 0-55: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/LetIn.v", line 4, characters 0-39: | |
| - Warning: Notations "_ + _" defined at level 50 with arguments constr | |
| - at level 50 and "_ +" defined at level 50 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/LetIn.v", line 4, characters 0-39: | |
| - Warning: Notations "_ * _" defined at level 40 with arguments constr | |
| - at level 40 and "_ *" defined at level 40 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/LetIn.v", line 4, characters 0-39: | |
| - Warning: Notations "_ [ ? ]" defined at level 9 with arguments constr | |
| - at next level and "_ [ _ ]" defined at level 30 with arguments constr | |
| - at next level have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/LetIn.v", line 4, characters 0-39: | |
| - Warning: Notations "slet _ .. _ <- _ ; _" defined at level 70 with arguments | |
| - binder and "slet _ .. _ := _ in _" defined at level 200 with arguments binder | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - src/Rewriter/Util/LetIn.vo (real: 0.18, user: 0.09, sys: 0.08, mem: 148500 ko) | |
| - ROCQ compile src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v", line 2, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v", line 3, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v", line 4, characters 0-28: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v", line 5, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v", line 6, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v", line 7, characters 0-51: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v", line 8, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v", line 9, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v", line 10, characters 0-30: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v", line 11, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Rewriter/Examples/PerfTesting/Sample.v", line 749, characters 0-289: | |
| - Warning: native_compute disabled at configure time; falling back to | |
| - vm_compute. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Rewriter/Examples/PerfTesting/Sample.vo (real: 0.57, user: 0.44, sys: 0.12, mem: 427504 ko) | |
| - ROCQ compile src/Rewriter/Util/InductiveHList.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/InductiveHList.vo (real: 0.15, user: 0.05, sys: 0.09, mem: 100668 ko) | |
| - ROCQ compile src/Rewriter/Util/HProp.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/HProp.vo (real: 0.16, user: 0.07, sys: 0.09, mem: 130528 ko) | |
| - ROCQ compile src/Rewriter/Util/Isomorphism.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Isomorphism.vo (real: 0.14, user: 0.06, sys: 0.08, mem: 96920 ko) | |
| - ROCQ compile src/Rewriter/Util/Equality.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/Equality.v", line 7, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Util/Equality.vo (real: 0.21, user: 0.11, sys: 0.10, mem: 215988 ko) | |
| - ROCQ compile src/Rewriter/Util/IffT.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/IffT.v", line 1, characters 0-40: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Util/IffT.vo (real: 0.15, user: 0.06, sys: 0.09, mem: 120740 ko) | |
| - ROCQ compile src/Rewriter/Util/PrimitiveProd.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/PrimitiveProd.v", line 8, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Util/PrimitiveProd.vo (real: 0.22, user: 0.09, sys: 0.13, mem: 259688 ko) | |
| - ROCQ compile src/Rewriter/Util/PrimitiveHList.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/PrimitiveHList.v", line 1, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Util/PrimitiveHList.vo (real: 0.19, user: 0.08, sys: 0.11, mem: 139688 ko) | |
| - ROCQ compile src/Rewriter/Language/PreCommon.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Language/PreCommon.v", line 5, characters 0-39: | |
| - Warning: Notations "_ + _" defined at level 50 with arguments constr | |
| - at level 50 and "_ +" defined at level 50 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/PreCommon.v", line 5, characters 0-39: | |
| - Warning: Notations "_ * _" defined at level 40 with arguments constr | |
| - at level 40 and "_ *" defined at level 40 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/PreCommon.v", line 5, characters 0-39: | |
| - Warning: Notations "_ [ ? ]" defined at level 9 with arguments constr | |
| - at next level and "_ [ _ ]" defined at level 30 with arguments constr | |
| - at next level have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/PreCommon.v", line 5, characters 0-39: | |
| - Warning: Notations "slet _ .. _ <- _ ; _" defined at level 70 with arguments | |
| - binder and "slet _ .. _ := _ in _" defined at level 200 with arguments binder | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/PreCommon.v", line 19, characters 16-86: | |
| - Warning: Unused variable: ctx_tys. [ltac2-unused-variable,ltac2,default] | |
| - File "./src/Rewriter/Language/PreCommon.v", line 20, characters 16-92: | |
| - Warning: Unused variable: ctx_tys. [ltac2-unused-variable,ltac2,default] | |
| - src/Rewriter/Language/PreCommon.vo (real: 0.20, user: 0.09, sys: 0.10, mem: 145100 ko) | |
| - ROCQ compile src/Rewriter/Language/Pre.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Language/Pre.v", line 2, characters 0-39: | |
| - Warning: Notations "_ + _" defined at level 50 with arguments constr | |
| - at level 50 and "_ +" defined at level 50 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/Pre.v", line 2, characters 0-39: | |
| - Warning: Notations "_ * _" defined at level 40 with arguments constr | |
| - at level 40 and "_ *" defined at level 40 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/Pre.v", line 2, characters 0-39: | |
| - Warning: Notations "_ [ ? ]" defined at level 9 with arguments constr | |
| - at next level and "_ [ _ ]" defined at level 30 with arguments constr | |
| - at next level have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/Pre.v", line 2, characters 0-39: | |
| - Warning: Notations "slet _ .. _ <- _ ; _" defined at level 70 with arguments | |
| - binder and "slet _ .. _ := _ in _" defined at level 200 with arguments binder | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - src/Rewriter/Language/Pre.vo (real: 0.20, user: 0.12, sys: 0.08, mem: 150936 ko) | |
| - ROCQ compile src/Rewriter/Util/Bool.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/Bool.v", line 2, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Bool.v", line 3, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Util/Bool.vo (real: 0.19, user: 0.10, sys: 0.08, mem: 184692 ko) | |
| - ROCQ compile src/Rewriter/Util/Comparison.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Comparison.vo (real: 0.15, user: 0.03, sys: 0.11, mem: 109268 ko) | |
| - ROCQ compile src/Rewriter/Util/Sigma.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Sigma.vo (real: 0.25, user: 0.14, sys: 0.11, mem: 310660 ko) | |
| - ROCQ compile src/Rewriter/Util/Decidable.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/Decidable.v", line 3, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Decidable.v", line 4, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Decidable.v", line 8, characters 0-42: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Decidable.v", line 9, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Decidable.v", line 14, characters 0-31: | |
| - Warning: The '%' scope delimiter in 'Arguments' commands is deprecated, use | |
| - '%_' instead (available since 8.19). The '%' syntax will be reused in a | |
| - future version with the same semantics as in terms, that is adding scope to | |
| - the stack for all subterms. Code can be adapted with a script like: for f in | |
| - $(find . -name '*.v'); do sed '/Arguments/ s/%/%_/g' -i $f ; done | |
| - [argument-scope-delimiter,deprecated-since-8.19,deprecated,default] | |
| - src/Rewriter/Util/Decidable.vo (real: 0.59, user: 0.46, sys: 0.13, mem: 391828 ko) | |
| - ROCQ compile src/Rewriter/Util/NatUtil.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 1, characters 0-27: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 2, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 3, characters 0-30: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 4, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 5, characters 0-45: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 6, characters 0-28: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 53, characters 35-42: | |
| - Warning: Notation mod_mod is deprecated since 8.17. Use Div0.mod_mod instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 192, characters 43-50: | |
| - Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 192, characters 43-50: | |
| - Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 221, characters 12-23: | |
| - Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 221, characters 12-23: | |
| - Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 221, characters 12-23: | |
| - Warning: Notation mod_add is deprecated since 8.17. Use Div0.mod_add instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 287, characters 28-36: | |
| - Warning: Notation mod_same is deprecated since 8.17. | |
| - Use Div0.mod_same instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 287, characters 28-36: | |
| - Warning: Notation mod_same is deprecated since 8.17. | |
| - Use Div0.mod_same instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 305, characters 10-17: | |
| - Warning: Notation add_mod is deprecated since 8.17. Use Div0.add_mod instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 305, characters 10-17: | |
| - Warning: Notation add_mod is deprecated since 8.17. Use Div0.add_mod instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 305, characters 10-17: | |
| - Warning: Notation add_mod is deprecated since 8.17. Use Div0.add_mod instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 332, characters 2-20: | |
| - Warning: Tactic Notation revert dependent (hyp) is deprecated since 8.18. | |
| - Use "generalize dependent" instead ("revert dependent" is currently an alias) | |
| - [deprecated-tactic-notation-since-8.18,deprecated-since-8.18,deprecated-tactic-notation,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 420, characters 20-27: | |
| - Warning: Notation mod_mul is deprecated since 8.17. Use Div0.mod_mul instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 420, characters 20-27: | |
| - Warning: Notation mod_mul is deprecated since 8.17. Use Div0.mod_mul instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 420, characters 20-27: | |
| - Warning: Notation mod_mul is deprecated since 8.17. Use Div0.mod_mul instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 447, characters 19-34: | |
| - Warning: Notation add_mod_idemp_r is deprecated since 8.17. | |
| - Use Div0.add_mod_idemp_r instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 447, characters 19-34: | |
| - Warning: Notation add_mod_idemp_r is deprecated since 8.17. | |
| - Use Div0.add_mod_idemp_r instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/NatUtil.v", line 447, characters 19-34: | |
| - Warning: Notation add_mod_idemp_r is deprecated since 8.17. | |
| - Use Div0.add_mod_idemp_r instead. | |
| - [deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default] | |
| - src/Rewriter/Util/NatUtil.vo (real: 0.70, user: 0.58, sys: 0.12, mem: 418012 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/Head.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/Head.vo (real: 0.15, user: 0.08, sys: 0.07, mem: 106348 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/BreakMatch.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/BreakMatch.vo (real: 0.16, user: 0.08, sys: 0.08, mem: 114284 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/DestructHyps.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/DestructHyps.vo (real: 0.16, user: 0.06, sys: 0.10, mem: 111076 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/DestructHead.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/DestructHead.vo (real: 0.17, user: 0.07, sys: 0.09, mem: 123076 ko) | |
| - ROCQ compile src/Rewriter/Util/Option.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/Option.v", line 1, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Option.v", line 2, characters 0-45: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Option.v", line 5, characters 0-39: | |
| - Warning: Notations "_ + _" defined at level 50 with arguments constr | |
| - at level 50 and "_ +" defined at level 50 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/Option.v", line 5, characters 0-39: | |
| - Warning: Notations "_ * _" defined at level 40 with arguments constr | |
| - at level 40 and "_ *" defined at level 40 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/Option.v", line 5, characters 0-39: | |
| - Warning: Notations "_ [ ? ]" defined at level 9 with arguments constr | |
| - at next level and "_ [ _ ]" defined at level 30 with arguments constr | |
| - at next level have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/Option.v", line 5, characters 0-39: | |
| - Warning: Notations "slet _ .. _ <- _ ; _" defined at level 70 with arguments | |
| - binder and "slet _ .. _ := _ in _" defined at level 200 with arguments binder | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - src/Rewriter/Util/Option.vo (real: 0.32, user: 0.21, sys: 0.11, mem: 314388 ko) | |
| - ROCQ compile src/Rewriter/Util/Pointed.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/Pointed.v", line 1, characters 0-32: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Util/Pointed.vo (real: 0.16, user: 0.08, sys: 0.08, mem: 129864 ko) | |
| - ROCQ compile src/Rewriter/Util/Prod.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/Prod.v", line 8, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Prod.v", line 9, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Prod.v", line 10, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Util/Prod.vo (real: 0.25, user: 0.15, sys: 0.09, mem: 268904 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/ConstrFail.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/ConstrFail.vo (real: 0.14, user: 0.06, sys: 0.08, mem: 95712 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/Test.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/Test.vo (real: 0.14, user: 0.07, sys: 0.07, mem: 95288 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/Not.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/Not.vo (real: 0.14, user: 0.05, sys: 0.09, mem: 94556 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/DoWithHyp.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/DoWithHyp.vo (real: 0.15, user: 0.06, sys: 0.09, mem: 106972 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/RewriteHyp.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/RewriteHyp.vo (real: 0.17, user: 0.07, sys: 0.10, mem: 139064 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/SpecializeBy.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/SpecializeBy.vo (real: 0.15, user: 0.05, sys: 0.10, mem: 108088 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/SplitInContext.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/SplitInContext.vo (real: 0.16, user: 0.06, sys: 0.09, mem: 107596 ko) | |
| - ROCQ compile src/Rewriter/Util/ListUtil.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 1, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2, characters 0-35: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 3, characters 0-28: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 4, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 5, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 6, characters 0-30: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 7, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 136, characters 3-13: | |
| - Warning: Notation app_length is deprecated since 8.20. | |
| - Use length_app instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 137, characters 3-13: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 138, characters 3-13: | |
| - Warning: Notation map_length is deprecated since 8.20. | |
| - Use length_map instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 139, characters 3-13: | |
| - Warning: Notation seq_length is deprecated since 8.20. | |
| - Use length_seq instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 140, characters 3-19: | |
| - Warning: Notation fold_left_length is deprecated since 8.20. | |
| - Use fold_left_S_0 instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 141, characters 3-17: | |
| - Warning: Notation split_length_l is deprecated since 8.20. | |
| - Use length_fst_split instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 142, characters 3-17: | |
| - Warning: Notation split_length_r is deprecated since 8.20. | |
| - Use length_snd_split instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 143, characters 3-16: | |
| - Warning: Notation firstn_length is deprecated since 8.20. | |
| - Use length_firstn instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 144, characters 3-17: | |
| - Warning: Notation combine_length is deprecated since 8.20. | |
| - Use length_combine instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 145, characters 3-14: | |
| - Warning: Notation prod_length is deprecated since 8.20. | |
| - Use length_prod instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 972, characters 40-54: | |
| - Warning: Notation combine_length is deprecated since 8.20. | |
| - Use length_combine instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 972, characters 40-54: | |
| - Warning: Notation combine_length is deprecated since 8.20. | |
| - Use length_combine instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 972, characters 40-54: | |
| - Warning: Notation combine_length is deprecated since 8.20. | |
| - Use length_combine instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 1980, characters 0-35: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2240, characters 67-85: | |
| - Warning: Tactic Notation revert dependent (hyp) is deprecated since 8.18. | |
| - Use "generalize dependent" instead ("revert dependent" is currently an alias) | |
| - [deprecated-tactic-notation-since-8.18,deprecated-since-8.18,deprecated-tactic-notation,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2246, characters 45-63: | |
| - Warning: Tactic Notation revert dependent (hyp) is deprecated since 8.18. | |
| - Use "generalize dependent" instead ("revert dependent" is currently an alias) | |
| - [deprecated-tactic-notation-since-8.18,deprecated-since-8.18,deprecated-tactic-notation,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2252, characters 45-63: | |
| - Warning: Tactic Notation revert dependent (hyp) is deprecated since 8.18. | |
| - Use "generalize dependent" instead ("revert dependent" is currently an alias) | |
| - [deprecated-tactic-notation-since-8.18,deprecated-since-8.18,deprecated-tactic-notation,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2377, characters 53-63: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2377, characters 53-63: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2377, characters 53-63: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2377, characters 53-63: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2377, characters 53-63: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2377, characters 53-63: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2377, characters 53-63: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2386, characters 10-25: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2386, characters 10-25: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2386, characters 10-25: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2389, characters 52-67: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2391, characters 31-46: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2389, characters 52-67: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2389, characters 52-67: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2391, characters 31-46: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2391, characters 31-46: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2406, characters 64-79: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2406, characters 64-79: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2406, characters 64-79: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2406, characters 64-79: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2406, characters 64-79: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2406, characters 64-79: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2407, characters 2-20: | |
| - Warning: Tactic Notation revert dependent (hyp) is deprecated since 8.18. | |
| - Use "generalize dependent" instead ("revert dependent" is currently an alias) | |
| - [deprecated-tactic-notation-since-8.18,deprecated-since-8.18,deprecated-tactic-notation,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2408, characters 36-51: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2408, characters 36-51: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil.v", line 2408, characters 36-51: | |
| - Warning: Notation rev_length is deprecated since 8.20. | |
| - Use length_rev instead. | |
| - [deprecated-syntactic-definition-since-8.20,deprecated-since-8.20,deprecated-syntactic-definition,deprecated,default] | |
| - src/Rewriter/Util/ListUtil.vo (real: 3.67, user: 3.50, sys: 0.16, mem: 466004 ko) | |
| - ROCQ compile src/Rewriter/Util/ListUtil/SetoidList.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/ListUtil/SetoidList.v", line 1, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil/SetoidList.v", line 2, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/ListUtil/SetoidList.v", line 3, characters 0-35: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Util/ListUtil/SetoidList.vo (real: 0.32, user: 0.20, sys: 0.12, mem: 356704 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/Contains.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/Contains.vo (real: 0.14, user: 0.08, sys: 0.06, mem: 95436 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/SetoidSubst.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/SetoidSubst.vo (real: 0.14, user: 0.06, sys: 0.08, mem: 98568 ko) | |
| - ROCQ compile src/Rewriter/Util/Sum.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/Sum.v", line 1, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Sum.v", line 2, characters 0-45: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Util/Sum.vo (real: 0.42, user: 0.28, sys: 0.14, mem: 391768 ko) | |
| - ROCQ compile src/Rewriter/Util/Bool/Reflect.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/Bool/Reflect.v", line 2, characters 0-35: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Bool/Reflect.v", line 3, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Bool/Reflect.v", line 4, characters 0-30: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Bool/Reflect.v", line 5, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Bool/Reflect.v", line 6, characters 0-40: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Bool/Reflect.v", line 7, characters 0-30: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Bool/Reflect.v", line 8, characters 0-42: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/Bool/Reflect.v", line 9, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - src/Rewriter/Util/Bool/Reflect.vo (real: 1.69, user: 1.53, sys: 0.16, mem: 428576 ko) | |
| - ROCQ compile src/Rewriter/Util/CPSNotations.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/CPSNotations.v", line 1, characters 0-39: | |
| - Warning: Notations "_ + _" defined at level 50 with arguments constr | |
| - at level 50 and "_ +" defined at level 50 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/CPSNotations.v", line 1, characters 0-39: | |
| - Warning: Notations "_ * _" defined at level 40 with arguments constr | |
| - at level 40 and "_ *" defined at level 40 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/CPSNotations.v", line 1, characters 0-39: | |
| - Warning: Notations "_ [ ? ]" defined at level 9 with arguments constr | |
| - at next level and "_ [ _ ]" defined at level 30 with arguments constr | |
| - at next level have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/CPSNotations.v", line 1, characters 0-39: | |
| - Warning: Notations "slet _ .. _ <- _ ; _" defined at level 70 with arguments | |
| - binder and "slet _ .. _ := _ in _" defined at level 200 with arguments binder | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - src/Rewriter/Util/CPSNotations.vo (real: 0.16, user: 0.07, sys: 0.09, mem: 119132 ko) | |
| - ROCQ compile src/Rewriter/Util/OptionList.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/OptionList.v", line 1, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Util/OptionList.v", line 3, characters 0-39: | |
| - Warning: Notations "_ + _" defined at level 50 with arguments constr | |
| - at level 50 and "_ +" defined at level 50 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/OptionList.v", line 3, characters 0-39: | |
| - Warning: Notations "_ * _" defined at level 40 with arguments constr | |
| - at level 40 and "_ *" defined at level 40 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/OptionList.v", line 3, characters 0-39: | |
| - Warning: Notations "_ [ ? ]" defined at level 9 with arguments constr | |
| - at next level and "_ [ _ ]" defined at level 30 with arguments constr | |
| - at next level have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Util/OptionList.v", line 3, characters 0-39: | |
| - Warning: Notations "slet _ .. _ <- _ ; _" defined at level 70 with arguments | |
| - binder and "slet _ .. _ := _ in _" defined at level 200 with arguments binder | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - src/Rewriter/Util/OptionList.vo (real: 0.25, user: 0.15, sys: 0.09, mem: 293016 ko) | |
| - ROCQ compile src/Rewriter/Language/Language.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Language/Language.v", line 1, characters 0-31: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Language/Language.v", line 2, characters 0-37: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Language/Language.v", line 3, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Language/Language.v", line 4, characters 0-29: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Language/Language.v", line 5, characters 0-34: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Language/Language.v", line 6, characters 0-45: | |
| - Warning: "From Coq" has been replaced by "From Stdlib". | |
| - [deprecated-from-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Language/Language.v", line 19, characters 0-39: | |
| - Warning: Notations "_ + _" defined at level 50 with arguments constr | |
| - at level 50 and "_ +" defined at level 50 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/Language.v", line 19, characters 0-39: | |
| - Warning: Notations "_ * _" defined at level 40 with arguments constr | |
| - at level 40 and "_ *" defined at level 40 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/Language.v", line 19, characters 0-39: | |
| - Warning: Notations "_ [ ? ]" defined at level 9 with arguments constr | |
| - at next level and "_ [ _ ]" defined at level 30 with arguments constr | |
| - at next level have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/Language.v", line 19, characters 0-39: | |
| - Warning: Notations "slet _ .. _ <- _ ; _" defined at level 70 with arguments | |
| - binder and "slet _ .. _ := _ in _" defined at level 200 with arguments binder | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/Language.v", line 20, characters 7-21: | |
| - Warning: Coq.Lists.List has been replaced by Stdlib.Lists.List. | |
| - [deprecated-dirpath-Coq,deprecated-since-9.0,deprecated,default] | |
| - File "./src/Rewriter/Language/Language.v", line 299, characters 2-41: | |
| - Warning: The '%' scope delimiter in 'Arguments' commands is deprecated, use | |
| - '%_' instead (available since 8.19). The '%' syntax will be reused in a | |
| - future version with the same semantics as in terms, that is adding scope to | |
| - the stack for all subterms. Code can be adapted with a script like: for f in | |
| - $(find . -name '*.v'); do sed '/Arguments/ s/%/%_/g' -i $f ; done | |
| - [argument-scope-delimiter,deprecated-since-8.19,deprecated,default] | |
| - File "./src/Rewriter/Language/Language.v", line 914, characters 6-97: | |
| - Warning: The '%' scope delimiter in 'Arguments' commands is deprecated, use | |
| - '%_' instead (available since 8.19). The '%' syntax will be reused in a | |
| - future version with the same semantics as in terms, that is adding scope to | |
| - the stack for all subterms. Code can be adapted with a script like: for f in | |
| - $(find . -name '*.v'); do sed '/Arguments/ s/%/%_/g' -i $f ; done | |
| - [argument-scope-delimiter,deprecated-since-8.19,deprecated,default] | |
| - src/Rewriter/Language/Language.vo (real: 0.88, user: 0.73, sys: 0.13, mem: 463364 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/FindHyp.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/FindHyp.vo (real: 0.15, user: 0.05, sys: 0.10, mem: 106924 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/UniquePose.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/UniquePose.vo (real: 0.15, user: 0.04, sys: 0.11, mem: 107068 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/SpecializeAllWays.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/SpecializeAllWays.vo (real: 0.15, user: 0.05, sys: 0.10, mem: 105784 ko) | |
| - ROCQ compile src/Rewriter/Language/Inversion.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Language/Inversion.v", line 15, characters 0-39: | |
| - Warning: Notations "_ + _" defined at level 50 with arguments constr | |
| - at level 50 and "_ +" defined at level 50 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/Inversion.v", line 15, characters 0-39: | |
| - Warning: Notations "_ * _" defined at level 40 with arguments constr | |
| - at level 40 and "_ *" defined at level 40 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/Inversion.v", line 15, characters 0-39: | |
| - Warning: Notations "_ [ ? ]" defined at level 9 with arguments constr | |
| - at next level and "_ [ _ ]" defined at level 30 with arguments constr | |
| - at next level have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/Inversion.v", line 15, characters 0-39: | |
| - Warning: Notations "slet _ .. _ <- _ ; _" defined at level 70 with arguments | |
| - binder and "slet _ .. _ := _ in _" defined at level 200 with arguments binder | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/Inversion.v", line 97, characters 6-24: | |
| - Warning: Tactic Notation revert dependent (hyp) is deprecated since 8.18. | |
| - Use "generalize dependent" instead ("revert dependent" is currently an alias) | |
| - [deprecated-tactic-notation-since-8.18,deprecated-since-8.18,deprecated-tactic-notation,deprecated,default] | |
| - File "./src/Rewriter/Language/Inversion.v", line 1044, characters 75-93: | |
| - Warning: Tactic Notation revert dependent (hyp) is deprecated since 8.18. | |
| - Use "generalize dependent" instead ("revert dependent" is currently an alias) | |
| - [deprecated-tactic-notation-since-8.18,deprecated-since-8.18,deprecated-tactic-notation,deprecated,default] | |
| - src/Rewriter/Language/Inversion.vo (real: 13.66, user: 13.49, sys: 0.16, mem: 566024 ko) | |
| - ROCQ compile src/Rewriter/Language/IdentifiersBasicLibrary.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Language/IdentifiersBasicLibrary.vo (real: 2.27, user: 2.15, sys: 0.12, mem: 490200 ko) | |
| - ROCQ compile src/Rewriter/Language/UnderLets.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Language/UnderLets.v", line 2, characters 0-39: | |
| - Warning: Notations "_ + _" defined at level 50 with arguments constr | |
| - at level 50 and "_ +" defined at level 50 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/UnderLets.v", line 2, characters 0-39: | |
| - Warning: Notations "_ * _" defined at level 40 with arguments constr | |
| - at level 40 and "_ *" defined at level 40 with arguments constr at next level | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/UnderLets.v", line 2, characters 0-39: | |
| - Warning: Notations "_ [ ? ]" defined at level 9 with arguments constr | |
| - at next level and "_ [ _ ]" defined at level 30 with arguments constr | |
| - at next level have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - File "./src/Rewriter/Language/UnderLets.v", line 2, characters 0-39: | |
| - Warning: Notations "slet _ .. _ <- _ ; _" defined at level 70 with arguments | |
| - binder and "slet _ .. _ := _ in _" defined at level 200 with arguments binder | |
| - have incompatible prefixes. One of them will likely not work. | |
| - [notation-incompatible-prefix,parsing,default] | |
| - src/Rewriter/Language/UnderLets.vo (real: 0.39, user: 0.24, sys: 0.14, mem: 438732 ko) | |
| - ROCQ compile src/Rewriter/Language/UnderLetsCacheProofs.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Language/UnderLetsCacheProofs.vo (real: 0.30, user: 0.21, sys: 0.09, mem: 348280 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/DebugPrint.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/DebugPrint.vo (real: 0.15, user: 0.05, sys: 0.10, mem: 116452 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics/RunTacticAsConstr.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics/RunTacticAsConstr.vo (real: 0.15, user: 0.07, sys: 0.08, mem: 105768 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics2/Array.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics2/Array.vo (real: 0.16, user: 0.07, sys: 0.08, mem: 102836 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics2/Iterate.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics2/Iterate.vo (real: 0.16, user: 0.06, sys: 0.09, mem: 102704 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics2/Option.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics2/Option.vo (real: 0.16, user: 0.07, sys: 0.08, mem: 102304 ko) | |
| - ROCQ compile src/Rewriter/Util/Tactics2/Proj.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - src/Rewriter/Util/Tactics2/Proj.vo (real: 0.16, user: 0.05, sys: 0.10, mem: 103732 ko) | |
| - ROCQ compile src/Rewriter/Util/plugins/Ltac2Extra.v | |
| - While loading initial state: | |
| - Warning: Native compiler is disabled, -native-compiler ondemand option | |
| - ignored. [native-compiler-disabled,native-compiler,default] | |
| - File "./src/Rewriter/Util/plugins/Ltac2Extra.v", line 3, characters 0-45: | |
| - Error: | |
| - System error: "src/Rewriter/Util/plugins/././ltac2_extra_plugin.cmxs: No such file or directory" | |
| - | |
| - Command exited with non-zero status 1 | |
| - src/Rewriter/Util/plugins/Ltac2Extra.vo (real: 0.16, user: 0.05, sys: 0.10, mem: 101912 ko) | |
| - make: *** [Makefile.coq:818: src/Rewriter/Util/plugins/Ltac2Extra.vo] Error 1 | |
| - make: *** [src/Rewriter/Util/plugins/Ltac2Extra.vo] Deleting file 'src/Rewriter/Util/plugins/Ltac2Extra.glob' | |
| <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> | |
| ┌─ The following actions failed | |
| │ λ build coq-rewriter-perf-SuperFast dev | |
| └─ | |
| ╶─ No changes have been performed |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment