diff options
| -rw-r--r-- | .circleci/config.yml | 159 | ||||
| -rw-r--r-- | checker/reduction.ml | 2 | ||||
| -rw-r--r-- | dev/doc/build-system.txt | 4 | ||||
| -rwxr-xr-x | dev/lint-commits.sh | 19 | ||||
| -rw-r--r-- | engine/eConstr.mli | 5 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 2 | ||||
| -rw-r--r-- | parsing/cLexer.ml4 | 3 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 6 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_theory.v | 2 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/timing/run.sh | 24 | ||||
| -rw-r--r-- | test-suite/output/bug6821.out | 2 | ||||
| -rw-r--r-- | test-suite/output/bug6821.v | 8 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 3 | ||||
| -rw-r--r-- | theories/Reals/Rpower.v | 25 |
16 files changed, 88 insertions, 180 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 441d89d42..352ec5a51 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -1,3 +1,7 @@ +# This file used to contain configuration to also build documentation and CoqIDE, +# run the test-suite and the validate targets, +# including with 32-bits architecture or bleeding-edge compiler. + defaults: params: ¶ms # Following parameters are used in Coq CircleCI Job (using yaml @@ -16,20 +20,8 @@ defaults: NATIVE_COMP: "yes" # some useful values - COMPILER_32BIT: &compiler-32bit "4.02.3+32bit" - - COMPILER_BLEEDING_EDGE: &compiler-be "4.06.0" - CAMLP5_VER_BLEEDING_EDGE: &camlp5-ver-be "7.03" - TIMING_PACKAGES: &timing-packages "time python" - COQIDE_PACKAGES: &coqide-packages "libgtk2.0-dev libgtksourceview2.0-dev" - #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" - COQIDE_OPAM: &coqide-opam "lablgtk-extras" - COQIDE_OPAM_BE: &coqide-opam-be "num lablgtk.2.18.6 lablgtk-extras.1.6" - COQDOC_PACKAGES: &coqdoc-packages "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa" - COQDOC_OPAM: &coqdoc-opam "hevea" - version: 2 before_script: &before_script @@ -38,7 +30,6 @@ before_script: &before_script echo export TERM=xterm >> ~/.profile source ~/.profile printenv - #if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -yq && sudo apt-get install -yq --no-install-recommends ${EXTRA_PACKAGES}; fi opam-switch: &opam-switch @@ -76,7 +67,7 @@ opam-switch: &opam-switch command: | source ~/.profile opam switch -j ${NJOBS} ${COMPILER} - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${COQIDE_OPAM} ${COQDOC_OPAM} ${EXTRA_OPAM} + opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} - run: name: Clean cache command: | @@ -104,7 +95,7 @@ opam-switch: &opam-switch command: | source ~/.profile - ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} + ./configure -local -native-compiler ${NATIVE_COMP} -coqide no - run: &build-build name: Build command: | @@ -117,53 +108,8 @@ opam-switch: &opam-switch paths: - coq/ - environment: &build-variables - <<: *envvars - EXTRA_CONF: "-coqide opt" - EXTRA_PACKAGES: *coqide-packages - -.validate-template: &validate-template - <<: *params - steps: - - run: *before_script - - attach_workspace: *attach_workspace - - run: - name: Validate - command: | - source ~/.profile - make validate environment: *envvars -.documentation-template: &documentation-template - <<: *params - steps: - - run: *before_script - - attach_workspace: *attach_workspace - - run: - name: Documentation - command: | - source ~/.profile - make -j ${NJOBS} doc - environment: &documentation-variables - <<: *envvars - EXTRA_PACKAGES: *coqdoc-packages - -.test-suite-template: &test-suite-template - <<: *params - steps: - - run: *before_script - - attach_workspace: *attach_workspace - - run: - name: Test - command: | - source ~/.profile - cd test-suite - make clean - make -j ${NJOBS} all - environment: &test-suite-variables - <<: *envvars - EXTRA_PACKAGES: *timing-packages - .ci-template: &ci-template <<: *params steps: @@ -184,84 +130,16 @@ opam-switch: &opam-switch # Defines individual jobs, see the workflows section below for job orchestration jobs: - # TODO: linter opam-boot: <<: *opam-boot-template environment: <<: *envvars - EXTRA_PACKAGES: *coqide-packages EXTRA_OPAM: "ocamlgraph ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" - opam-boot-32bit: - <<: *opam-boot-template - environment: - <<: *envvars - EXTRA_PACKAGES: "gcc-multilib" - COMPILER: *compiler-32bit - COQIDE_OPAM: "" - COQDOC_OPAM: "" - - opam-boot-be: - <<: *opam-boot-template - environment: - <<: *envvars - EXTRA_PACKAGES: *coqide-packages - COMPILER: *compiler-be - CAMLP5_VER: *camlp5-ver-be - COQIDE_OPAM: *coqide-opam-be - # Build and prepare test environment build: *build-template - build-32bit: - <<: *build-template - environment: - <<: *envvars # no coqide for 32bit - EXTRA_PACKAGES: "gcc-multilib" - COMPILER: *compiler-32bit - - build-be: - <<: *build-template - environment: - <<: *build-variables - COMPILER: *compiler-be - - validate: *validate-template - - validate-32bit: - <<: *validate-template - environment: - <<: *envvars - COMPILER: *compiler-32bit - EXTRA_PACKAGES: "gcc-multilib" - - documentation: *documentation-template - - documentation-be: - <<: *documentation-template - environment: - <<: *documentation-variables - COMPILER: *compiler-be - CAMLP5_VER: *camlp5-ver-be - - test-suite: - <<: *test-suite-template - - test-suite-32bit: - <<: *test-suite-template - environment: - <<: *test-suite-variables - COMPILER: *compiler-32bit - EXTRA_PACKAGES: "gcc-multilib time python" - - test-suite-be: - <<: *test-suite-template - environment: - <<: *test-suite-variables - COMPILER: *compiler-be - EXTRA_PACKAGES: *timing-packages - bignums: <<: *ci-template @@ -352,19 +230,14 @@ workflows: main: jobs: - opam-boot - - opam-boot-32bit - - opam-boot-be - build: requires: - opam-boot - - validate: &req-main + + - bignums: &req-main requires: - build - - test-suite: *req-main - - documentation: *req-main - - - bignums: *req-main - color: requires: - build @@ -397,19 +270,3 @@ workflows: - sf: *req-main - unimath: *req-main - vst: *req-main - - - build-32bit: - requires: - - opam-boot-32bit - - validate-32bit: &req-32bit - requires: - - build-32bit - - test-suite-32bit: *req-32bit - - - build-be: - requires: - - opam-boot-be - - test-suite-be: &req-be - requires: - - build-be - - documentation-be: *req-be diff --git a/checker/reduction.ml b/checker/reduction.ml index 2297c90b3..d7d742d8a 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -582,7 +582,6 @@ let dest_prod_assum env = | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in prodec_rec (push_rel d env) (d::l) c - | Cast (c,_,_) -> prodec_rec env l c | _ -> let rty' = whd_all env rty in if Term.eq_constr rty' rty then l, rty @@ -600,7 +599,6 @@ let dest_lam_assum env = | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in lamec_rec (push_rel d env) (d::l) c - | Cast (c,_,_) -> lamec_rec env l c | _ -> l,rty in lamec_rec env empty_rel_context diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 1c4fd2eba..fd3101613 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -143,7 +143,9 @@ file list(s): These files are also used by the experimental ocamlbuild plugin, which is quite touchy about them : be careful with order, duplicated entries, whitespace errors, and do not mention .mli there. - - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) + If module B depends on module A, then B should be after A in the .mllib + file. +- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) - The definitions in Makefile.common might have to be adapted too. - If your file needs a specific rule, add it to Makefile.build diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh index eb12bc227..d8043558e 100755 --- a/dev/lint-commits.sh +++ b/dev/lint-commits.sh @@ -19,14 +19,21 @@ fi BASE_COMMIT="$1" HEAD_COMMIT="$2" -# git diff --check -# uses .gitattributes to know what to check -if git diff --check "$BASE_COMMIT" "$HEAD_COMMIT"; +bad=() +while IFS= read -r commit; do + echo Checking "$commit" + # git diff --check + # uses .gitattributes to know what to check + if ! git diff --check "${commit}^" "$commit"; + then + bad+=("$commit") + fi +done < <(git rev-list "$HEAD_COMMIT" --not "$BASE_COMMIT" --) + +if [ "${#bad[@]}" != 0 ] then - : -else >&2 echo "Whitespace errors!" - >&2 echo "Running 'git diff --check $BASE_COMMIT $HEAD_COMMIT'." + >&2 echo "In commits ${bad[*]}" >&2 echo "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces." exit 1 fi diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 6fa338c73..01847fe07 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -67,7 +67,10 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term val to_constr : Evd.evar_map -> t -> Constr.t -(** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *) +(** Returns the evar-normal form of the argument, and cast it as a theoretically + evar-free term. In practice this function does not check that the result + is actually evar-free, it is currently the duty of the caller to do so. + This might change in the future. *) val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index c65f4785e..9bc41a996 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1132,7 +1132,7 @@ let rec match_ inner u alp metas sigma a1 a2 = else f1,l1, f2, l2 in let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in List.fold_left2 (match_ may_use_eta u alp metas) - (match_in u alp metas sigma f1 f2) l1 l2 + (match_hd u alp metas sigma f1 f2) l1 l2 | GLambda (na1,bk1,t1,b1), NLambda (na2,t2,b2) -> match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in u alp metas sigma t1 t2) b1 b2 | GProd (na1,bk1,t1,b1), NProd (na2,t2,b2) -> diff --git a/kernel/reduction.ml b/kernel/reduction.ml index da7042713..68f53c355 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -918,7 +918,6 @@ let dest_prod_assum env = | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in prodec_rec (push_rel d env) (Context.Rel.add d l) c - | Cast (c,_,_) -> prodec_rec env l c | _ -> let rty' = whd_all env rty in if Constr.equal rty' rty then l, rty @@ -936,7 +935,6 @@ let dest_lam_assum env = | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in lamec_rec (push_rel d env) (Context.Rel.add d l) c - | Cast (c,_,_) -> lamec_rec env l c | _ -> l,rty in lamec_rec env Context.Rel.empty diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index f26398fa9..52a6fe16c 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -404,8 +404,9 @@ let set_lexer_state (o,s,b,c,f) = between_commands := b; comments := c; current_file := f -let release_lexer_state () = +let get_lexer_state () = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file) +let release_lexer_state = get_lexer_state let drop_lexer_state () = set_lexer_state (init_lexer_state Loc.ToplevelInput) diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index d3ef19873..5f4e10f14 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -51,7 +51,9 @@ type lexer_state val init_lexer_state : Loc.source -> lexer_state val set_lexer_state : lexer_state -> unit +val get_lexer_state : unit -> lexer_state val release_lexer_state : unit -> lexer_state +[@@ocaml.deprecated "Use get_lexer_state"] val drop_lexer_state : unit -> unit (* Retrieve the comments lexed at a given location of the stream diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index ddb26d771..7a51908d9 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -111,7 +111,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct let state = ref (CLexer.init_lexer_state file) in CLexer.set_lexer_state !state; let a = parsable c in - state := CLexer.release_lexer_state (); + state := CLexer.get_lexer_state (); (a,state) let action = Gramext.action @@ -121,7 +121,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct CLexer.set_lexer_state !state; try let c = Entry.parse e p in - state := CLexer.release_lexer_state (); + state := CLexer.get_lexer_state (); c with Ploc.Exc (loc,e) -> CLexer.drop_lexer_state (); @@ -133,7 +133,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct CLexer.set_lexer_state !state; try let a = f x in - state := CLexer.release_lexer_state (); + state := CLexer.get_lexer_state (); a with e -> CLexer.drop_lexer_state (); diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 776ebd808..14aead045 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -263,7 +263,7 @@ Section ALMOST_RING. Variable SRth : semi_ring_theory 0 1 radd rmul req. (** Every semi ring can be seen as an almost ring, by taking : - -x = x and x - y = x + y *) + [-x = x] and [x - y = x + y] *) Definition SRopp (x:R) := x. Notation "- x" := (SRopp x). Definition SRsub x y := x + -y. Infix "-" := SRsub. diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 2439d3f37..aa6b0a9a4 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -38,9 +38,29 @@ make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $? INFINITY="∞" INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase +TO_SED_IN_BOTH=( + -e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent + -e s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent + -e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces + -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out + -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators +) + +TO_SED_IN_PER_FILE=( + -e s'/[0-9]//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start + -e s'/ */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start + -e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign +) + +TO_SED_IN_PER_LINE=( + -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start + -e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives + -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs + ) + for ext in "" .desired; do for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do - cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed + cat ${file}${ext} | grep -v 'warning: undefined variable' | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed done done for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do @@ -74,7 +94,7 @@ echo for ext in "" .desired; do for file in A.v.timing.diff; do - cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/ *$//g' | sed s'/+/-/g' | sort > ${file}${ext}.processed + cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed done done for file in A.v.timing.diff; do diff --git a/test-suite/output/bug6821.out b/test-suite/output/bug6821.out new file mode 100644 index 000000000..7b12b5320 --- /dev/null +++ b/test-suite/output/bug6821.out @@ -0,0 +1,2 @@ +forall f : nat -> Type, f x where x : nat := 1 + : Type diff --git a/test-suite/output/bug6821.v b/test-suite/output/bug6821.v new file mode 100644 index 000000000..40627e331 --- /dev/null +++ b/test-suite/output/bug6821.v @@ -0,0 +1,8 @@ +(* Was failing at printing time with stack overflow due to an infinite + eta-expansion *) + +Notation "x 'where' y .. z := v " := + ((fun y => .. ((fun z => x) v) ..) v) + (at level 11, v at next level, y binder, z binder). + +Check forall f, f x where x := 1. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 7bcd2799a..bc82c3712 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1611,6 +1611,9 @@ Proof. Qed. Hint Resolve mult_INR: real. +Lemma pow_INR (m n: nat) : INR (m ^ n) = pow (INR m) n. +Proof. now induction n as [|n IHn];[ | simpl; rewrite mult_INR, IHn]. Qed. + (*********) Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n. Proof. diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index a646104cd..301fe20b0 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -431,9 +431,9 @@ Proof. Qed. Theorem Rpower_lt : - forall x y z:R, 1 < x -> 0 <= y -> y < z -> x ^R y < x ^R z. + forall x y z:R, 1 < x -> y < z -> x ^R y < x ^R z. Proof. - intros x y z H H0 H1. + intros x y z H H1. unfold Rpower. apply exp_increasing. apply Rmult_lt_compat_r. @@ -488,11 +488,13 @@ Proof. Qed. Theorem Rle_Rpower : - forall e n m:R, 1 < e -> 0 <= n -> n <= m -> e ^R n <= e ^R m. + forall e n m:R, 1 <= e -> n <= m -> e ^R n <= e ^R m. Proof. - intros e n m H H0 H1; case H1. - intros H2; left; apply Rpower_lt; assumption. - intros H2; rewrite H2; right; reflexivity. + intros e n m [H | H]; intros H1. + case H1. + intros H2; left; apply Rpower_lt; assumption. + intros H2; rewrite H2; right; reflexivity. + now rewrite <- H; unfold Rpower; rewrite ln_1, !Rmult_0_r; apply Rle_refl. Qed. Theorem ln_lt_2 : / 2 < ln 2. @@ -707,13 +709,18 @@ intros x y z x0 y0; unfold Rpower. rewrite <- exp_plus, ln_mult, Rmult_plus_distr_l; auto. Qed. -Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> Rpower a c <= Rpower b c. +Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> a ^R c < b ^R c. +Proof. +intros c0 [a0 ab]; apply exp_increasing. +now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier. +Qed. + +Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> a ^R c <= b ^R c. Proof. intros [c0 | c0]; [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ]. intros [a0 [ab|ab]]. - left; apply exp_increasing. - now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier. + now apply Rlt_le, Rlt_Rpower_l;[ | split]; fourier. rewrite ab; apply Rle_refl. apply Rlt_le_trans with a; tauto. tauto. |