diff options
| -rw-r--r-- | Makefile.build | 4 | ||||
| -rw-r--r-- | Makefile.dune | 35 | ||||
| -rw-r--r-- | dev/ci/README-developers.md | 35 | ||||
| -rw-r--r-- | doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst | 8 | ||||
| -rw-r--r-- | doc/changelog/08-tools/12211-time-ocaml.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/using/libraries/writing.rst | 2 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 108 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12196.v | 46 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_6378.v | 9 | ||||
| -rw-r--r-- | test-suite/success/ltacprof.v | 17 | ||||
| -rw-r--r-- | theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v | 313 | ||||
| -rw-r--r-- | theories/Sorting/CPermutation.v | 2 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 24 |
14 files changed, 369 insertions, 257 deletions
diff --git a/Makefile.build b/Makefile.build index b7a4dd655a..cf9141853d 100644 --- a/Makefile.build +++ b/Makefile.build @@ -249,8 +249,8 @@ MLINCLUDES=$(LOCALINCLUDES) USERCONTRIBINCLUDES=$(addprefix -I user-contrib/,$(USERCONTRIBDIRS)) -OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) -OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) +OCAMLC := $(TIMER) $(OCAMLFIND) ocamlc $(CAMLFLAGS) +OCAMLOPT := $(TIMER) $(OCAMLFIND) opt $(CAMLFLAGS) BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS) diff --git a/Makefile.dune b/Makefile.dune index b002c7709d..c2899dcaba 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -1,7 +1,7 @@ # -*- mode: makefile -*- # Dune Makefile for Coq -.PHONY: help states world watch check # Main developer targets +.PHONY: help help-install states world watch check # Main developer targets .PHONY: refman-html refman-pdf stdlib-html apidoc # Documentation targets .PHONY: test-suite .PHONY: fmt ocheck ireport clean # Maintenance targets @@ -11,6 +11,7 @@ # DUNEOPT=--display=short help: + @echo "" @echo "Welcome to Coq's Dune-based build system. Common developer targets are:" @echo "" @echo " - states: build a minimal functional coqtop" @@ -19,8 +20,15 @@ help: @echo " - check: build all ML files as fast as possible" @echo " - test-suite: run Coq's test suite" @echo "" - @echo " Note: these targets produce a developer build," - @echo " not suitable for distribution to end-users" + @echo " Note: running ./configure is not recommended," + @echo " see dev/doc/build-system.dune.md for more info" + @echo " Note: these targets produce a developer build, not suitable" + @echo " for distribution to end-users or install" + @echo "" + @echo " To run an \$$app \\in {coqc,coqtop,coqbyte,coqide}:" + @echo "" + @echo " - use 'dune exec -- dev/shim/\$$app-prelude args'" + @echo " Example: 'dune exec -- dev/shim/coqc-prelude file.v'" @echo "" @echo " Documentation targets:" @echo "" @@ -37,9 +45,14 @@ help: @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" @echo "" - @echo " To run an app \\in {coqc,coqtop,coqbyte,coqide}:" + @echo " Type 'make help-install' for installation instructions" + +help-install: + @echo "" + @echo "The Dune-based Coq build is split in packages; see Dune and dev/doc" + @echo "documentation for more details. A quick install of Coq alone can done with" @echo "" - @echo " - use 'dune exec -- dev/shim/app-prelude args'" + @echo " ./configure -prefix <install_prefix> && dune build -p coq && dune install -p coq" @echo "" @echo " Provided opam/dune packages are:" @echo "" @@ -52,8 +65,16 @@ help: @echo " - 'dune build package.install' : build package in developer mode" @echo " - 'dune build -p package' : build package in release mode" @echo "" - @echo " Packages _must_ be installed using release mode, use: 'dune install -p package'" - @echo " See Dune documentation for more information." + @echo " Packages _must_ be installed using release mode, to install a package use: " + @echo "" + @echo " - 'dune install -p package'" + @echo "" + @echo " Example: " + @echo "" + @echo " - 'dune build -p coq,coqide-server,coqide && dune install -p coq coqide-server coqide'" + @echo "" + @echo " Note that building a package in release mode ignores other packages present in" + @echo " the worktree. See Dune documentation for more information." voboot: @echo "This target is empty and not needed anymore" diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 88d08a1724..d5c6096100 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -73,16 +73,31 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil If you break external projects that are hosted on GitHub, you can use the `create_overlays.sh` script to automatically perform most of the -above steps. In order to do so, call the script as: -``` -./dev/tools/create_overlays.sh ejgallego 9873 aac_tactics elpi ltac -``` -replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR -number. The script will: +above steps. In order to do so: -- checkout the contributions and prepare the branch/remote so you can - just commit the fixes and push, -- add the corresponding overlay file in `dev/ci/user-overlays`. +- determine the list of failing projects: +IDs can be found as ci-XXX1 ci-XXX2 ci-XXX3 in the list of GitLab CI failures; +- for each project XXXi, look in [ci-basic-overlay.sh](https://github.com/coq/coq/blob/master/dev/ci/ci-basic-overlay.sh) +to see if the corresponding `XXXi_CI_GITURL` is hosted on GitHub; +- log on GitHub and fork all the XXXi projects hosted there; +- call the script as: + + ``` + ./dev/tools/create_overlays.sh ejgallego 9873 XXX1 XXX2 XXX3 + ``` + + replacing `ejgallego` by your GitHub nickname, `9873` by the actual PR +number, and selecting the XXXi hosted on GitHub. The script will: + + + checkout the contributions and prepare the branch/remote so you can + just commit the fixes and push, + + add the corresponding overlay file in `dev/ci/user-overlays`; + +- go to `_build_ci/XXXi` to prepare your overlay +(you can test your modifications by using `make -C ../.. ci-XXXi`) +and push using `git push ejgallego` (replacing `ejgallego` by your GitHub nickname); +- finally push the `dev/ci/user-overlays/9873-elgallego-YYY.sh` file on your Coq fork +(replacing `9873` by the actual PR number, and `ejgallego` by your GitHub nickname). For problems related to ML-plugins, if you use `dune build` to build Coq, it will actually be aware of the broken contributions and perform @@ -124,7 +139,7 @@ Currently available artifacts are: - the Coq documentation, built in the `doc:*` jobs. When submitting a documentation PR, this can help reviewers checking the rendered result. **@coqbot** will automatically post links to these - artifacts in the PR checks section. Furthemore, these artifacts are + artifacts in the PR checks section. Furthermore, these artifacts are automatically deployed at: + Coq's Reference Manual [master branch]: diff --git a/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst b/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst new file mode 100644 index 0000000000..b90c8e7a1f --- /dev/null +++ b/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst @@ -0,0 +1,8 @@ +- **Fixed:** + The :flag:`Ltac Profiling` machinery now correctly handles + backtracking into multi-success tactics. The call-counts of some + tactics are unfortunately inflated by 1, as some tactics are + implicitly implemented as :g:`tac + fail`, which has two + entry-points rather than one (Fixes `#12196 + <https://github.com/coq/coq/issues/12196>`_, `#12197 + <https://github.com/coq/coq/pull/12197>`_, by Jason Gross). diff --git a/doc/changelog/08-tools/12211-time-ocaml.rst b/doc/changelog/08-tools/12211-time-ocaml.rst new file mode 100644 index 0000000000..7ff68cc495 --- /dev/null +++ b/doc/changelog/08-tools/12211-time-ocaml.rst @@ -0,0 +1,5 @@ +- **Changed:** + When passing ``TIMED=1`` to ``make`` with either Coq's own makefile + or a ``coq_makefile``\-made makefile, timing information is now + printed for OCaml files as well (`#12211 + <https://github.com/coq/coq/pull/12211>`_, by Jason Gross). diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 8418e9c73d..b184311bef 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1786,16 +1786,22 @@ performance issue. and allow displaying and resetting the profile from tactic scripts for benchmarking purposes. +.. warn:: Ltac Profiler encountered an invalid stack (no \ + self node). This can happen if you reset the profile during \ + tactic execution + + Currently, :tacn:`reset ltac profile` is not very well-supported, + as it clears all profiling information about all tactics, including + ones above the current tactic. As a result, the profiler has + trouble understanding where it is in tactic execution. This mixes + especially poorly with backtracking into multi-success tactics. In + general, non-top-level calls to :tacn:`reset ltac profile` should + be avoided. + You can also pass the ``-profile-ltac`` command line option to ``coqc``, which turns the :flag:`Ltac Profiling` flag on at the beginning of each document, and performs a :cmd:`Show Ltac Profile` at the end. -.. warning:: - - Note that the profiler currently does not handle backtracking into - multi-success tactics, and issues a warning to this effect in many cases - when such backtracking occurs. - Run-time optimization tactic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 801d492acb..325ea2af60 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -62,7 +62,7 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)` Definition bar x := S x. #[deprecated(since="1.2", note="Use bar instead.")] - Notation foo := bar. + Notation foo := bar (only parsing). Then, the following code still works, but emits a warning: diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 14fab251d0..0dbf16a821 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -25,27 +25,20 @@ let is_profiling = Flags.profile_ltac let set_profiling b = is_profiling := b let get_profiling () = !is_profiling -(** LtacProf cannot yet handle backtracking into multi-success tactics. - To properly support this, we'd have to somehow recreate our location in the - call-stack, and stop/restart the intervening timers. This is tricky and - possibly expensive, so instead we currently just emit a warning that - profiling results will be off. *) -let encountered_multi_success_backtracking = ref false - -let warn_profile_backtracking = - CWarnings.create ~name:"profile-backtracking" ~category:"ltac" - (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \ - into multi-success tactics; profiling results may be wildly inaccurate.") - -let warn_encountered_multi_success_backtracking () = - if !encountered_multi_success_backtracking then - warn_profile_backtracking () - -let encounter_multi_success_backtracking () = - if not !encountered_multi_success_backtracking +let encountered_invalid_stack_no_self = ref false + +let warn_invalid_stack_no_self = + CWarnings.create ~name:"profile-invalid-stack-no-self" ~category:"ltac" + (fun () -> strbrk + "Ltac Profiler encountered an invalid stack (no self \ + node). This can happen if you reset the profile during \ + tactic execution.") + +let encounter_invalid_stack_no_self () = + if not !encountered_invalid_stack_no_self then begin - encountered_multi_success_backtracking := true; - warn_encountered_multi_success_backtracking () + encountered_invalid_stack_no_self := true; + warn_invalid_stack_no_self () end @@ -76,8 +69,7 @@ module Local = Summary.Local let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root] let reset_profile_tmp () = - Local.(stack := [empty_treenode root]); - encountered_multi_success_backtracking := false + Local.(stack := [empty_treenode root]) (* ************** XML Serialization ********************* *) @@ -218,7 +210,6 @@ let to_string ~filter ?(cutoff=0.0) node = cumulate tree; !global in - warn_encountered_multi_success_backtracking (); let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in let msg = h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ @@ -296,13 +287,15 @@ let exit_tactic ~count_call start_time c = match Local.(!stack) with | [] | [_] -> (* oops, our stack is invalid *) - encounter_multi_success_backtracking (); + encounter_invalid_stack_no_self (); reset_profile_tmp () | node :: (parent :: rest as full_stack) -> let name = string_of_call c in if not (String.equal name node.name) then (* oops, our stack is invalid *) - encounter_multi_success_backtracking (); + CErrors.anomaly + (Pp.strbrk "Ltac Profiler encountered an invalid stack (wrong self node) \ + likely due to backtracking into multi-success tactics."); let node = { node with total = node.total +. diff; local = node.local +. diff; @@ -332,38 +325,56 @@ let exit_tactic ~count_call start_time c = (* Calls are over, we reset the stack and send back data *) if rest == [] && get_profiling () then begin assert(String.equal root parent.name); + encountered_invalid_stack_no_self := false; reset_profile_tmp (); feedback_results parent end -let tclFINALLY tac (finally : unit Proofview.tactic) = +(** [tclWRAPFINALLY before tac finally] runs [before] before each + entry-point of [tac] and passes the result of [before] to + [finally], which is then run at each exit-point of [tac], + regardless of whether it succeeds or fails. Said another way, if + [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun + ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with + [e], it behaves as [before >>= fun v -> finally v <*> tclZERO + e]. *) +let rec tclWRAPFINALLY before tac finally = + let open Proofview in let open Proofview.Notations in - Proofview.tclIFCATCH - tac - (fun v -> finally <*> Proofview.tclUNIT v) - (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn) + before >>= fun v -> tclCASE tac >>= function + | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e + | Next (ret, tac') -> tclOR + (finally v >>= fun () -> tclUNIT ret) + (fun e -> tclWRAPFINALLY before (tac' e) finally) let do_profile s call_trace ?(count_call=true) tac = let open Proofview.Notations in - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - if !is_profiling then - match call_trace, Local.(!stack) with - | (_, c) :: _, parent :: rest -> - let name = string_of_call c in - let node = get_child name parent in - Local.(stack := node :: parent :: rest); - Some (time ()) - | _ :: _, [] -> assert false - | _ -> None - else None)) >>= function - | Some start_time -> - tclFINALLY - tac + (* We do an early check to [is_profiling] so that we save the + overhead of [tclWRAPFINALLY] when profiling is not set + *) + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function + | false -> tac + | true -> + tclWRAPFINALLY (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - (match call_trace with - | (_, c) :: _ -> exit_tactic ~count_call start_time c - | [] -> ())))) - | None -> tac + if !is_profiling then + match call_trace, Local.(!stack) with + | (_, c) :: _, parent :: rest -> + let name = string_of_call c in + let node = get_child name parent in + Local.(stack := node :: parent :: rest); + Some (time ()) + | _ :: _, [] -> assert false + | _ -> None + else None))) + tac + (function + | Some start_time -> + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + (match call_trace with + | (_, c) :: _ -> exit_tactic ~count_call start_time c + | [] -> ())))) + | None -> Proofview.tclUNIT ()) (* ************** Accumulation of data from workers ************************* *) @@ -396,6 +407,7 @@ let _ = | _ -> ())) let reset_profile () = + encountered_invalid_stack_no_self := false; reset_profile_tmp (); data := SM.empty diff --git a/test-suite/bugs/closed/bug_12196.v b/test-suite/bugs/closed/bug_12196.v new file mode 100644 index 0000000000..c0851b3204 --- /dev/null +++ b/test-suite/bugs/closed/bug_12196.v @@ -0,0 +1,46 @@ +(** TODO: Figure out how to test "sanity" for the ltac profiler output *) +Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => n * fact n' end. +Fixpoint walk (n : nat) := match n with 0 => tt | S n => walk n end. +Ltac slow := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)). +Ltac slow2 := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)). +Ltac multi := idtac + slow + slow2. +Set Ltac Profiling. +Goal True. + Time try (multi; fail). + (* Warning: Ltac Profiler cannot yet handle backtracking into multi-success + tactics; profiling results may be wildly inaccurate. + [profile-backtracking,ltac] *) + Show Ltac Profile. + (* Used to be: +total time: 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 47.1% 47.1% 1 0.000s +─slow ---------------------------------- 35.3% 35.3% 1 0.000s +─slow2 --------------------------------- 17.6% 17.6% 1 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 47.1% 47.1% 1 0.000s +─slow ---------------------------------- 35.3% 35.3% 1 0.000s +─slow2 --------------------------------- 17.6% 17.6% 1 0.000s + + *) + (* Now: +total time: 2.074s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 0.0% 100.0% 6 1.119s +─slow ---------------------------------- 54.0% 54.0% 3 1.119s +─slow2 --------------------------------- 46.0% 46.0% 3 0.955s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 0.0% 100.0% 6 1.119s + ├─slow -------------------------------- 54.0% 54.0% 3 1.119s + └─slow2 ------------------------------- 46.0% 46.0% 3 0.955s + +*) +Abort. diff --git a/test-suite/bugs/closed/bug_6378.v b/test-suite/bugs/closed/bug_6378.v index 68ae7961dd..453924d587 100644 --- a/test-suite/bugs/closed/bug_6378.v +++ b/test-suite/bugs/closed/bug_6378.v @@ -7,11 +7,20 @@ Ltac profile_constr tac := Ltac slow _ := eval vm_compute in (Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl). +Ltac manipulate_ltac_prof := + start ltac profiling; + reset ltac profile; + try ((idtac + reset ltac profile + idtac); fail); + try ((idtac + start ltac profiling + idtac); fail); + try ((idtac + stop ltac profiling + idtac); fail). + Goal True. start ltac profiling. reset ltac profile. + manipulate_ltac_prof. reset ltac profile. stop ltac profiling. + Set Warnings Append "+profile-invalid-stack-no-self". time profile_constr slow. show ltac profile cutoff 0. show ltac profile "slow". diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v index d5552695c4..f40f40c2bb 100644 --- a/test-suite/success/ltacprof.v +++ b/test-suite/success/ltacprof.v @@ -6,3 +6,20 @@ Goal True. try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *) Admitted. Show Ltac Profile. + +(* backtracking across profiler manipulation *) +Unset Ltac Profiling. +Reset Ltac Profile. + +Fixpoint slow (n : nat) : unit + := match n with + | 0 => tt + | S n => fst (slow n, slow n) + end. + +Ltac slow := idtac; let v := eval cbv in (slow 16) in idtac. +Ltac multi2 := + try (((idtac; slow) + (start ltac profiling; slow) + (idtac; slow) + (slow; stop ltac profiling; slow) + slow + (start ltac profiling; (idtac + slow); ((stop ltac profiling + idtac); fail))); slow; fail); slow; show ltac profile. +Goal True. + multi2. +Admitted. diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v index 5fc3a0e653..f4daedcb97 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v @@ -189,49 +189,63 @@ Proof. intros. rewrite CReal_mult_comm. apply CReal_mult_0_r. Qed. -Lemma CReal_mult_lt_0_compat : forall x y : CReal, - inject_Q 0 < x - -> inject_Q 0 < y - -> inject_Q 0 < x * y. +Lemma CRealLt_0_aboveSig : forall (x : CReal) (n : positive), + Qlt (2 # n) (proj1_sig x n) + -> forall p:positive, + Pos.le n p -> Qlt (1 # n) (proj1_sig x p). +Proof. + intros. destruct x as [xn caux]. + unfold proj1_sig. unfold proj1_sig in H. + specialize (caux n n p (Pos.le_refl n) H0). + apply (Qplus_lt_l _ _ (xn n-xn p)). + apply (Qlt_trans _ ((1#n) + (1#n))). + apply Qplus_lt_r. exact (Qle_lt_trans _ _ _ (Qle_Qabs _) caux). + rewrite Qinv_plus_distr. ring_simplify. exact H. +Qed. + +(* Correctness lemma for the Definition CReal_mult_lt_0_compat below. *) +Lemma CReal_mult_lt_0_compat_correct + : forall (x y : CReal) (H : 0 < x) (H0 : 0 < y), + (2 # 2 * proj1_sig H * proj1_sig H0 < + proj1_sig (x * y)%CReal (2 * proj1_sig H * proj1_sig H0)%positive - + proj1_sig (inject_Q 0) (2 * proj1_sig H * proj1_sig H0)%positive)%Q. Proof. - intros. destruct H as [x0 H], H0 as [x1 H0]. - pose proof (CRealLt_aboveSig (inject_Q 0) x x0 H). - pose proof (CRealLt_aboveSig (inject_Q 0) y x1 H0). + intros. + destruct H as [x0 H], H0 as [x1 H0]. unfold proj1_sig. + unfold inject_Q, proj1_sig, Qminus in H. rewrite Qplus_0_r in H. + pose proof (CRealLt_0_aboveSig x x0 H) as H1. + unfold inject_Q, proj1_sig, Qminus in H0. rewrite Qplus_0_r in H0. + pose proof (CRealLt_0_aboveSig y x1 H0) as H2. destruct x as [xn limx], y as [yn limy]; simpl in H, H1, H2, H0. - pose proof (QCauchySeq_bounded_prop xn limx) as majx. - pose proof (QCauchySeq_bounded_prop yn limy) as majy. - destruct (Qarchimedean (/ (xn x0 - 0 - (2 # x0)))). - destruct (Qarchimedean (/ (yn x1 - 0 - (2 # x1)))). - exists (Pos.max x0 x~0 * Pos.max x1 x2~0)%positive. - simpl. + unfold CReal_mult, inject_Q, proj1_sig. remember (QCauchySeq_bound xn id) as Ax. remember (QCauchySeq_bound yn id) as Ay. unfold Qminus. rewrite Qplus_0_r. - unfold Qminus in H1, H2. - specialize (H1 ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive). - assert (Pos.max x1 x2~0 <= (Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive. - { rewrite Pos.mul_assoc. - rewrite <- (Pos.mul_1_l (Pos.max x1 x2~0)). - rewrite Pos.mul_assoc. apply Pos.mul_le_mono_r. discriminate. } - specialize (H2 ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive H3). - rewrite Qplus_0_r in H1, H2. - apply (Qlt_trans _ ((2 # Pos.max x0 x~0) * (2 # Pos.max x1 x2~0))). - unfold Qlt; simpl. assert (forall p : positive, (Z.pos p < Z.pos p~0)%Z). - intro p. rewrite <- (Z.mul_1_l (Z.pos p)). - replace (Z.pos p~0) with (2 * Z.pos p)%Z. apply Z.mul_lt_mono_pos_r. - apply Pos2Z.is_pos. reflexivity. reflexivity. - apply H4. - apply (Qlt_trans _ ((2 # Pos.max x0 x~0) * (yn ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive))). - apply Qmult_lt_l. reflexivity. apply H2. apply Qmult_lt_r. - apply (Qlt_trans 0 (2 # Pos.max x1 x2~0)). reflexivity. apply H2. - apply H1. rewrite Pos.mul_comm. apply Pos2Nat.inj_le. - rewrite <- Pos.mul_assoc. rewrite Pos2Nat.inj_mul. - rewrite <- (mult_1_r (Pos.to_nat (Pos.max x0 x~0))). - rewrite <- mult_assoc. apply Nat.mul_le_mono_nonneg. - apply le_0_n. apply le_refl. auto. - rewrite mult_1_l. apply Pos2Nat.is_pos. + specialize (H2 (2 * (Pos.max Ax Ay) * (2 * x0 * x1))%positive). + setoid_replace (2 # 2 * x0 * x1)%Q with ((1#x0) * (1#x1))%Q. + assert (x0 <= 2 * Pos.max Ax Ay * (2 * x0 * x1))%positive. + { apply (Pos.le_trans _ (2 * Pos.max Ax Ay * x0)). + apply belowMultiple. apply Pos.mul_le_mono_l. + rewrite (Pos.mul_comm 2 x0), <- Pos.mul_assoc, Pos.mul_comm. + apply belowMultiple. } + apply (Qlt_trans _ (xn (2 * Pos.max Ax Ay * (2 * x0 * x1))%positive * (1#x1))). + - apply Qmult_lt_compat_r. reflexivity. apply H1, H3. + - apply Qmult_lt_l. + apply (Qlt_trans _ (1#x0)). reflexivity. apply H1, H3. + apply H2. apply (Pos.le_trans _ (2 * Pos.max Ax Ay * x1)). + apply belowMultiple. apply Pos.mul_le_mono_l. apply belowMultiple. + - unfold Qeq, Qmult, Qnum, Qden. + rewrite Z.mul_1_l, <- Pos2Z.inj_mul. reflexivity. Qed. +(* Strict inequality on CReal is in sort Type, for example + used in the computation of division. *) +Definition CReal_mult_lt_0_compat : forall x y : CReal, + 0 < x -> 0 < y -> 0 < x * y + := fun x y H H0 => exist _ (2 * proj1_sig H * proj1_sig H0)%positive + (CReal_mult_lt_0_compat_correct + x y H H0). + Lemma CReal_mult_bound_indep : forall (x y : CReal) (A : positive) (xbound : forall n : positive, (Qabs (proj1_sig x n) < Z.pos A # 1)%Q) @@ -777,22 +791,22 @@ Qed. Lemma CReal_mult_eq_reg_l : forall (r r1 r2 : CReal), r # 0 - -> CRealEq (CReal_mult r r1) (CReal_mult r r2) - -> CRealEq r1 r2. + -> r * r1 == r * r2 + -> r1 == r2. Proof. intros. destruct H; split. - intro abs. apply (CReal_mult_lt_compat_l (-r)) in abs. rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs. - exact (CRealLt_irrefl _ abs). apply (CReal_plus_lt_reg_l r). + exact (CRealLe_refl _ abs). apply (CReal_plus_lt_reg_l r). rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact c. - intro abs. apply (CReal_mult_lt_compat_l (-r)) in abs. rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs. - exact (CRealLt_irrefl _ abs). apply (CReal_plus_lt_reg_l r). + exact (CRealLe_refl _ abs). apply (CReal_plus_lt_reg_l r). rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact c. - intro abs. apply (CReal_mult_lt_compat_l r) in abs. rewrite H0 in abs. - exact (CRealLt_irrefl _ abs). exact c. + exact (CRealLe_refl _ abs). exact c. - intro abs. apply (CReal_mult_lt_compat_l r) in abs. rewrite H0 in abs. - exact (CRealLt_irrefl _ abs). exact c. + exact (CRealLe_refl _ abs). exact c. Qed. Lemma CReal_abs_appart_zero : forall (x : CReal) (n : positive), @@ -904,98 +918,60 @@ Proof. (proj1_sig d (Pos.of_nat (S n)) - proj1_sig c (Pos.of_nat (S n)))); assumption. Qed. -Lemma CRealShiftReal : forall (x : CReal) (k : positive), - QCauchySeq (fun n => proj1_sig x (Pos.max n k)). -Proof. - intros x k n p q H0 H1. - destruct x as [xn cau]; unfold proj1_sig. - apply cau. exact (Pos.le_trans _ _ _ H0 (Pos.le_max_l _ _)). - exact (Pos.le_trans _ _ _ H1 (Pos.le_max_l _ _)). -Qed. - -Lemma CRealShiftEqual : forall (x : CReal) (k : positive), - x == exist _ (fun n => proj1_sig x (Pos.max n k)) (CRealShiftReal x k). -Proof. - intros. split. - - intros [n maj]. destruct x as [xn cau]; simpl in maj. - specialize (cau n (Pos.max n k) n (Pos.le_max_l _ _ ) (Pos.le_refl _)). - apply (Qlt_not_le _ _ maj). clear maj. - apply (Qle_trans _ (Qabs (xn (Pos.max n k) - xn n))). - apply Qle_Qabs. apply Qlt_le_weak. apply (Qlt_trans _ _ _ cau). - unfold Qlt, Qnum, Qden. - apply Z.mul_lt_mono_pos_r. reflexivity. reflexivity. - - intros [n maj]. destruct x as [xn cau]; simpl in maj. - specialize (cau n (Pos.max n k) n (Pos.le_max_l _ _ ) (Pos.le_refl _)). - apply (Qlt_not_le _ _ maj). clear maj. - rewrite Qabs_Qminus in cau. - apply (Qle_trans _ (Qabs (xn n - xn (Pos.max n k)))). - apply Qle_Qabs. apply Qlt_le_weak. apply (Qlt_trans _ _ _ cau). - unfold Qlt, Qnum, Qden. - apply Z.mul_lt_mono_pos_r. reflexivity. reflexivity. -Qed. - -(* Find a positive negative real number, which rational sequence - stays above 0, so that it can be inversed. *) -Definition CRealPosShift (x : CReal) (xPos : 0 < x) : positive - := let (n,maj) := xPos in - let (a,_) := Qarchimedean (/ (proj1_sig x n - 0 - (2 # n))) in - Pos.max n (2*a). - +(* Find a positive index after which the Cauchy sequence proj1_sig x + stays above 0, so that it can be inverted. *) Lemma CRealPosShift_correct : forall (x : CReal) (xPos : 0 < x) (n : positive), - Qlt (1 # CRealPosShift x xPos) (proj1_sig x (Pos.max n (CRealPosShift x xPos))). -Proof. - intros x xPos p. unfold CRealPosShift. - pose proof (CRealLt_aboveSig 0 x) as H. - destruct xPos as [n maj], x as [xn cau]; simpl in maj. - unfold inject_Q, proj1_sig in H. specialize (H n maj). - simpl. - destruct (Qarchimedean (/ (xn n - 0 - (2 # n)))) as [a _]. - apply (Qlt_trans _ (2 # (Pos.max n (2*a)))). - apply Z.mul_lt_mono_pos_r; reflexivity. - specialize (H (Pos.max p (Pos.max n (2*a))) (Pos.le_max_r _ _)). - apply (Qlt_le_trans _ _ _ H). ring_simplify. apply Qle_refl. + Pos.le (proj1_sig xPos) n + -> Qlt (1 # proj1_sig xPos) (proj1_sig x n). +Proof. + intros x xPos p pmaj. + destruct xPos as [n maj]; simpl in maj. + apply (CRealLt_0_aboveSig x n). + unfold proj1_sig in pmaj. + apply (Qlt_le_trans _ _ _ maj). + ring_simplify. apply Qle_refl. apply pmaj. Qed. -Lemma CReal_inv_pos_cauchy : forall (x : CReal) (xPos : 0 < x), - QCauchySeq (fun n : positive - => / proj1_sig x (Pos.max ((CRealPosShift x xPos) ^ 2 * n) - (CRealPosShift x xPos))). +Lemma CReal_inv_pos_cauchy + : forall (x : CReal) (xPos : 0 < x) (k : positive), + (forall n:positive, Pos.le k n -> Qlt (1 # k) (proj1_sig x n)) + -> QCauchySeq (fun n : positive => / proj1_sig x (k ^ 2 * n)%positive). Proof. - intros. - remember (CRealPosShift x xPos) as k. - pose (fun n : positive => proj1_sig x (Pos.max n k)) as yn. - pose proof (CRealShiftReal x k) as cau. - pose proof (CRealPosShift_correct x xPos) as maj. + intros [xn xcau] xPos k maj. unfold proj1_sig. intros n p q H0 H1. - setoid_replace - (/ proj1_sig x (Pos.max (k ^ 2 * p) k) - / proj1_sig x (Pos.max (k ^ 2 * q) k))%Q - with ((yn (k ^ 2 * q)%positive - - yn (k ^ 2 * p)%positive) - / (yn (k ^ 2 * q)%positive * - yn (k ^ 2 * p)%positive)). - + apply (Qle_lt_trans _ (Qabs (yn (k ^ 2 * q)%positive - - yn (k ^ 2 * p)%positive) + setoid_replace (/ xn (k ^ 2 * p)%positive - / xn (k ^ 2 * q)%positive)%Q + with ((xn (k ^ 2 * q)%positive - + xn (k ^ 2 * p)%positive) + / (xn (k ^ 2 * q)%positive * + xn (k ^ 2 * p)%positive)). + + apply (Qle_lt_trans _ (Qabs (xn (k ^ 2 * q)%positive + - xn (k ^ 2 * p)%positive) / (1 # (k^2)))). - rewrite <- Heqk in maj. assert (1 # k ^ 2 - < Qabs (yn (k ^ 2 * q)%positive * yn (k ^ 2 * p)%positive))%Q. + < Qabs (xn (k ^ 2 * q)%positive * xn (k ^ 2 * p)%positive))%Q. { rewrite Qabs_Qmult. unfold "^"%positive; simpl. rewrite factorDenom. rewrite Pos.mul_1_r. - apply (Qlt_trans _ ((1#k) * Qabs (yn (k * k * p)%positive))). + apply (Qlt_trans _ ((1#k) * Qabs (xn (k * k * p)%positive))). apply Qmult_lt_l. reflexivity. rewrite Qabs_pos. specialize (maj (k * k * p)%positive). - apply maj. apply (Qle_trans _ (1 # k)). + apply maj. rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. + apply (Qle_trans _ (1 # k)). discriminate. apply Zlt_le_weak. apply maj. + rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. apply Qmult_lt_r. apply (Qlt_trans 0 (1#k)). reflexivity. rewrite Qabs_pos. specialize (maj (k * k * p)%positive). - apply maj. apply (Qle_trans _ (1 # k)). discriminate. + apply maj. rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. + apply (Qle_trans _ (1 # k)). discriminate. apply Zlt_le_weak. apply maj. + rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. rewrite Qabs_pos. specialize (maj (k * k * q)%positive). - apply maj. apply (Qle_trans _ (1 # k)). discriminate. - apply Zlt_le_weak. apply maj. } + apply maj. rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. + apply (Qle_trans _ (1 # k)). discriminate. + apply Zlt_le_weak. + apply maj. rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. } unfold Qdiv. rewrite Qabs_Qmult. rewrite Qabs_Qinv. rewrite Qmult_comm. rewrite <- (Qmult_comm (/ (1 # k ^ 2))). apply Qmult_le_compat_r. apply Qlt_le_weak. @@ -1004,37 +980,40 @@ Proof. rewrite Qmult_comm. apply Qlt_shift_div_l. reflexivity. rewrite Qmult_1_l. apply H. apply Qabs_nonneg. simpl in maj. - specialize (cau (n * (k^2))%positive - (k ^ 2 * q)%positive - (k ^ 2 * p)%positive). + pose proof (xcau (n * (k^2))%positive + (k ^ 2 * q)%positive + (k ^ 2 * p)%positive). apply Qlt_shift_div_r. reflexivity. - apply (Qlt_le_trans _ (1 # n * k ^ 2)). apply cau. + apply (Qlt_le_trans _ (1 # n * k ^ 2)). apply xcau. rewrite Pos.mul_comm. unfold id. apply Pos.mul_le_mono_l. exact H1. unfold id. rewrite Pos.mul_comm. apply Pos.mul_le_mono_l. exact H0. rewrite factorDenom. apply Qle_refl. - + unfold yn. field. split. intro abs. + + field. split. intro abs. specialize (maj (k ^ 2 * p)%positive). - rewrite <- Heqk in maj. - rewrite abs in maj. inversion maj. + rewrite abs in maj. apply (Qlt_not_le (1#k) 0). + apply maj. unfold "^"%positive; simpl. rewrite <- Pos.mul_assoc. + rewrite Pos.mul_comm. apply belowMultiple. discriminate. intro abs. specialize (maj (k ^ 2 * q)%positive). - rewrite <- Heqk in maj. - rewrite abs in maj. inversion maj. + rewrite abs in maj. apply (Qlt_not_le (1#k) 0). + apply maj. unfold "^"%positive; simpl. rewrite <- Pos.mul_assoc. + rewrite Pos.mul_comm. apply belowMultiple. discriminate. Qed. Definition CReal_inv_pos (x : CReal) (xPos : 0 < x) : CReal - := exist _ (fun n : positive - => / proj1_sig x (Pos.max ((CRealPosShift x xPos) ^ 2 * n) - (CRealPosShift x xPos))) - (CReal_inv_pos_cauchy x xPos). + := exist _ + (fun n : positive => / proj1_sig x (proj1_sig xPos ^ 2 * n)%positive) + (CReal_inv_pos_cauchy + x xPos (proj1_sig xPos) (CRealPosShift_correct x xPos)). -Lemma CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x. +Definition CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x. Proof. - intros. apply (CReal_plus_lt_reg_l x). - rewrite (CReal_plus_opp_r x), CReal_plus_0_r. exact H. -Qed. + intros x [n nmaj]. exists n. + apply (Qlt_le_trans _ _ _ nmaj). destruct x. simpl. + unfold Qminus. rewrite Qplus_0_l, Qplus_0_r. apply Qle_refl. +Defined. Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal := match xnz with @@ -1051,35 +1030,30 @@ Proof. intros. unfold CReal_inv. simpl. destruct rnz. - exfalso. apply CRealLt_asym in H. contradiction. - - remember (CRealPosShift r c) as k. - unfold CReal_inv_pos. - pose (CRealPosShift_correct r c) as maj. - rewrite <- Heqk in maj. - pose (fun n => proj1_sig r (Pos.max n (CRealPosShift r c))) as rn. + - unfold CReal_inv_pos. + pose proof (CRealPosShift_correct r c) as maj. destruct r as [xn cau]. unfold CRealLt; simpl. - destruct (Qarchimedean (rn 1%positive)) as [A majA]. + destruct (Qarchimedean (xn 1%positive)) as [A majA]. exists (2 * (A + 1))%positive. unfold Qminus. rewrite Qplus_0_r. - simpl in rn. rewrite <- Heqk. - rewrite <- (Qmult_1_l (/ xn (Pos.max (k ^ 2 * (2 * (A + 1))) k))). - apply Qlt_shift_div_l. apply (Qlt_trans 0 (1#k)). reflexivity. - apply maj. rewrite <- (Qmult_inv_r (Z.pos A + 1 # 1)). + rewrite <- (Qmult_1_l (/ xn (proj1_sig c ^ 2 * (2 * (A + 1)))%positive)). + apply Qlt_shift_div_l. apply (Qlt_trans 0 (1# proj1_sig c)). reflexivity. + apply maj. unfold "^"%positive, Pos.iter. + rewrite <- Pos.mul_assoc, Pos.mul_comm. apply belowMultiple. + rewrite <- (Qmult_inv_r (Z.pos A + 1 # 1)). setoid_replace (2 # 2 * (A + 1))%Q with (Qinv (Z.pos A + 1 # 1)). 2: reflexivity. rewrite Qmult_comm. apply Qmult_lt_r. reflexivity. - rewrite <- (Qplus_lt_l _ _ (- rn 1%positive)). - apply (Qle_lt_trans _ (Qabs (rn (k ^ 2 * (2 * (A + 1)))%positive + - rn 1%positive))). - unfold rn. rewrite <- Heqk. + rewrite <- (Qplus_lt_l _ _ (- xn 1%positive)). + apply (Qle_lt_trans _ (Qabs (xn (proj1_sig c ^ 2 * (2 * (A + 1)))%positive + - xn 1%positive))). apply Qle_Qabs. apply (Qlt_le_trans _ 1). apply cau. - rewrite <- Heqk. - destruct (Pos.max (k ^ 2 * (2 * (A + 1))) k)%positive; discriminate. - apply Pos.le_max_l. + apply Pos.le_1_l. apply Pos.le_1_l. rewrite <- Qinv_plus_distr. rewrite <- (Qplus_comm 1). rewrite <- Qplus_0_r. rewrite <- Qplus_assoc. rewrite <- Qplus_assoc. rewrite Qplus_le_r. rewrite Qplus_0_l. apply Qlt_le_weak. apply Qlt_minus_iff in majA. apply majA. intro abs. inversion abs. -Qed. +Defined. Lemma CReal_linear_shift : forall (x : CReal) (k : positive), QCauchySeq (fun n => proj1_sig x (k * n)%positive). @@ -1111,34 +1085,33 @@ Lemma CReal_inv_l_pos : forall (r:CReal) (rnz : 0 < r), (CReal_inv_pos r rnz) * r == 1. Proof. intros r c. - remember (CRealPosShift r c) as k. unfold CReal_inv_pos. pose proof (CRealPosShift_correct r c) as maj. - rewrite <- Heqk in maj. - pose (exist (fun x => QCauchySeq x) - (fun n => proj1_sig r (Pos.max n k)) (CRealShiftReal r k)) - as rshift. rewrite (CReal_mult_proper_l - _ r (exist _ (fun n => proj1_sig rshift (k ^ 2 * n)%positive) - (CReal_linear_shift rshift _))). - 2: rewrite <- CReal_linear_shift_eq; apply CRealShiftEqual. - assert (le 1 (Pos.to_nat k * (Pos.to_nat k * 1))%nat). rewrite mult_1_r. - { rewrite <- Pos2Nat.inj_mul. apply Pos2Nat.is_pos. } + _ r (exist _ (fun n => proj1_sig r (proj1_sig c ^ 2 * n)%positive) + (CReal_linear_shift r _))). + 2: rewrite <- CReal_linear_shift_eq; apply reflexivity. apply CRealEq_diff. intro n. destruct r as [rn limr]. - unfold CReal_mult, rshift, inject_Q, proj1_sig. - rewrite <- Heqk, Qmult_comm, Qmult_inv_r. + unfold CReal_mult, inject_Q, proj1_sig. + rewrite Qmult_comm, Qmult_inv_r. unfold Qminus. rewrite Qplus_opp_r, Qabs_pos. - discriminate. apply Qle_refl. intro abs. + discriminate. apply Qle_refl. unfold proj1_sig in maj. - remember (QCauchySeq_bound - (fun n0 : positive => / rn (Pos.max (k ^ 2 * n0) k)) - id)%Q as x. - remember (QCauchySeq_bound - (fun n0 : positive => rn (Pos.max (k ^ 2 * n0) k)%positive) - id) as x0. - specialize (maj ((k * (k * 1) * (Pos.max x x0 * n)~0)%positive)). - simpl in maj. rewrite abs in maj. inversion maj. + intro abs. + specialize (maj ((let (a, _) := c in a) ^ 2 * + (2 * + Pos.max + (QCauchySeq_bound + (fun n : positive => Qinv (rn ((let (a, _) := c in a) ^ 2 * n))) id) + (QCauchySeq_bound + (fun n : positive => rn ((let (a, _) := c in a) ^ 2 * n)) id) * n))%positive). + simpl in maj. unfold proj1_sig in maj, abs. + rewrite abs in maj. clear abs. + apply (Qlt_not_le (1 # (let (a, _) := c in a)) 0). + apply maj. unfold "^"%positive, Pos.iter. + rewrite <- Pos.mul_assoc, Pos.mul_comm. apply belowMultiple. + discriminate. Qed. Lemma CReal_inv_l : forall (r:CReal) (rnz : r # 0), diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v index fac9cd1d6d..21d04da877 100644 --- a/theories/Sorting/CPermutation.v +++ b/theories/Sorting/CPermutation.v @@ -154,7 +154,7 @@ Qed. Lemma CPermutation_length_1 : forall a b, CPermutation [a] [b] -> a = b. Proof. intros; now apply Permutation_length_1, CPermutation_Permutation. Qed. -Lemma CPermutation_length_1_inv : forall l a, CPermutation [a] l -> l = [a]. +Lemma CPermutation_length_1_inv : forall a l, CPermutation [a] l -> l = [a]. Proof. intros; now apply Permutation_length_1_inv, CPermutation_Permutation. Qed. Lemma CPermutation_swap : forall a b, CPermutation [a; b] [b; a]. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 57ba036a62..a26eb9dfbe 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -647,7 +647,7 @@ archclean:: $(MLIFILES:.mli=.cmi): %.cmi: %.mli $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< $(MLGFILES:.mlg=.ml): %.ml: %.mlg $(SHOW)'COQPP $<' @@ -656,53 +656,53 @@ $(MLGFILES:.mlg=.ml): %.ml: %.mlg # Stupid hack around a deficient syntax: we cannot concatenate two expansions $(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< # Same hack $(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< + $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< $(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -linkall -shared -o $@ $< $(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -shared -linkall -o $@ $< $(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< $(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack $(SHOW)'CAMLC -pack -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack $(SHOW)'CAMLOPT -pack -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ # This rule is for _CoqProject with no .mllib nor .mlpack $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -shared -o $@ $< ifneq (,$(TIMING)) |