Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293; Default flags for all Rocq libraries.(env ; cf explanation for warning settings in configure.ml (dev (flags :standard -w +a-4-9-27-40..42-44-45-48-58-67-68-70 -warn-error +a \ -short-paths) (rocq (flags :standard -w +default))) (release (flags :standard) (ocamlopt_flags :standard -O3)) (ireport (flags :standard -w -9-27+60-70) (ocamlopt_flags :standard -O3 -inlining-report)))
; Information about flags for release mode:;; In #9665 we tried to add (c_flags -O3) to the release setup,; unfortunately the resulting VM seems to be slower [5% slower on; fourcolor, thus we keep the default C flags for now, which seem to; be -O2.
; The _ profile could help factoring the above, however it doesn't; seem to work like we'd expect/like:;; (_ (flags :standard)))
(alias (name default) (deps rocq-runtime.install coq-core.install rocq-core.install rocqide-server.install))
(alias (name runtime) (deps rocq-runtime.install coq-core.install))
(install (section lib) (package rocq-runtime) (files revision))
(rule (targets revision) (mode fallback) (deps (:rev-script dev/tools/make_git_revision.sh)) (action (with-stdout-to revision (bash %{rev-script}))))
; bootstrap for theories/Corelib/dune(rule (targets corelib_dune) (deps (source_tree plugins) (source_tree theories)) (action (with-stdout-to %{targets} (run tools/dune_rule_gen/gen_rules.exe Corelib theories/Corelib %{env:COQ_DUNE_EXTRA_OPT=}))))
(rule (targets ltac2_dune) (deps (source_tree plugins) (source_tree theories)) (action (with-stdout-to %{targets} (run tools/dune_rule_gen/gen_rules.exe Ltac2 theories/Ltac2 -noinit %{env:COQ_DUNE_EXTRA_OPT=}))))
(rule (targets corelib_dune_split) (deps (source_tree plugins) (source_tree theories)) (action (with-stdout-to %{targets} (run tools/dune_rule_gen/gen_rules.exe Corelib theories/Corelib -split %{env:COQ_DUNE_EXTRA_OPT=}))))
(rule (targets ltac2_dune_split) (deps (source_tree plugins) (source_tree theories)) (action (with-stdout-to %{targets} (run tools/dune_rule_gen/gen_rules.exe Ltac2 theories/Ltac2 -noinit -split %{env:COQ_DUNE_EXTRA_OPT=}))))
; Use summary.log as the target(alias (name runtest) (package rocq-test-suite) (deps test-suite/summary.log))
; For make compat(alias (name all-src) (deps (source_tree theories) (source_tree plugins)))
; (dirs (:standard _build_ci))