Skip to content
Commits on Source (32)
Show whitespace changes
Inline Side-by-side
.bintray.json deleted 100644 → 0
View file @ 11d2b496
{
"package": {
"name": "coq",
"repo": "coq",
"subject": "coq"
},
"version": {
"name": "8.8.2"
},
"files":
[
{"includePattern": "_build/(.*\\.dmg)", "uploadPattern": "$1",
"matrixParams": {
"override": 1 }
}
],
"publish": true
}
.github/PULL_REQUEST_TEMPLATE.md
View file @ a7783b2b
......@@ -10,7 +10,10 @@
Fixes / closes #????
<!-- If there is a user-visible change in coqc/coqtop/coqchk/coq_makefile behavior and testing is not prohibitively expensive: -->
<!-- (Otherwise, remove this line.) -->
- [ ] Added / updated test-suite
<!-- If this is a feature pull request / breaks compatibility: -->
<!-- (Otherwise, remove these lines.) -->
- [ ] Corresponding documentation was added / updated.
- [ ] Entry added in CHANGES.
- [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
- [ ] Entry added in CHANGES.md.
.gitlab-ci.yml
View file @ a7783b2b
......@@ -9,12 +9,13 @@ stages:
variables:
# Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
# for reference]
CACHEKEY: "bionic_coq-v8.8-V2018-09-20"
CACHEKEY: "bionic_coq-v8.9-V2018-10-22"
IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
# By default, jobs run in the base switch; override to select another switch
OPAM_SWITCH: "base"
# Used to select special compiler switches such as flambda, 32bits, etc...
OPAM_VARIANT: ""
GIT_DEPTH: "10"
docker-boot:
stage: docker
......@@ -37,11 +38,11 @@ docker-boot:
before_script:
- cat /proc/{cpu,mem}info || true
- ls -a # figure out if artifacts are around
- printenv | sort
- printenv -0 | sort -z | tr '\0' '\n'
- declare -A switch_table
- switch_table=( ["base"]="$COMPILER" ["edge"]="$COMPILER_EDGE" )
- opam switch -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
- eval $(opam config env)
- opam switch set -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
- eval $(opam env)
- opam list
- opam config list
......@@ -60,23 +61,28 @@ after_script:
paths:
- _install_ci
- config/Makefile
- config/coq_config.py
- test-suite/misc/universes/all_stdlib.v
expire_in: 1 week
script:
- set -e
- echo 'start:coq.clean'
- make clean # ensure that `make clean` works on a fresh clone
- echo 'end:coq.clean'
- echo 'start:coq.config'
- ./configure -warn-error yes -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
- echo 'end:coq.config'
- echo 'start:coq.build'
- make -j "$NJOBS" byte
- make -j "$NJOBS"
- make -j "$NJOBS" world $EXTRA_TARGET
- make test-suite/misc/universes/all_stdlib.v
- echo 'end:coq:build'
- echo 'start:coq.install'
- make install
- make install install-byte $EXTRA_INSTALL
- make install-byte
- cp bin/fake_ide _install_ci/bin/
- echo 'end:coq.install'
......@@ -88,6 +94,19 @@ after_script:
# purpose, we add a spurious dependency `not-a-real-job` that must be
# overridden otherwise the CI will fail.
.doc-template: &doc-template
stage: test
dependencies:
- not-a-real-job
script:
- SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no'
- make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman
- make install-doc-sphinx
artifacts:
name: "$CI_JOB_NAME"
paths:
- _install_ci/share/doc/coq/
# set dependencies when using
.test-suite-template: &test-suite-template
stage: test
......@@ -155,12 +174,15 @@ after_script:
- call dev/ci/gitlab.bat
only:
variables:
- $WINDOWS == "enabled"
- $WINDOWS =~ /enabled/
build:base:
<<: *build-template
variables:
COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes"
COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
# coqdoc for stdlib, until we know how to build it from installed Coq
EXTRA_TARGET: "stdlib"
EXTRA_INSTALL: "install-doc-stdlib-html install-doc-printable"
# no coqide for 32bit: libgtk installation problems
build:base+32bit:
......@@ -225,6 +247,42 @@ pkg:nix:
paths:
- nix-build-coq.drv-0/*/test-suite/logs
build:macOS:
stage: build
artifacts:
name: "$CI_JOB_NAME"
paths:
- _build
expire_in: 1 week
tags:
- macOS
dependencies: []
before_script: []
script:
- dev/build/osx/make-macos-dmg.sh
variables:
NJOBS: "2"
only:
variables:
- $MACOS == "enabled"
doc:refman:
<<: *doc-template
dependencies:
- build:base
doc:ml-api:
stage: test
dependencies:
- build:edge
script:
- ./configure -warn-error yes -prefix "$(pwd)/_install_ci"
- make mli-doc source-doc # ml-doc [broken in 4.07.0]
artifacts:
name: "$CI_JOB_NAME"
paths:
- dev/ocamldoc
test-suite:base:
<<: *test-suite-template
dependencies:
......@@ -297,6 +355,9 @@ ci-coq-dpdgraph:
ci-coquelicot:
<<: *ci-template
ci-cross-crypto:
<<: *ci-template
ci-elpi:
<<: *ci-template
......@@ -336,12 +397,15 @@ ci-ltac2:
ci-math-comp:
<<: *ci-template-flambda
ci-quickchick:
<<: *ci-template-flambda
ci-mtac2:
<<: *ci-template
ci-pidetop:
<<: *ci-template
ci-quickchick:
<<: *ci-template-flambda
ci-sf:
<<: *ci-template
......
.merlin → .merlin.in
View file @ a7783b2b
......@@ -10,8 +10,6 @@ S kernel
B kernel
S kernel/byterun
B kernel/byterun
S intf
B intf
S library
B library
S engine
......@@ -34,6 +32,8 @@ S vernac
B vernac
S toplevel
B toplevel
S topbin
B topbin
S plugins/ltac
B plugins/ltac
S API
......
.travis.yml deleted 100644 → 0
View file @ 11d2b496
dist: trusty
# Travis builds are slower using sudo: false (the container-based
# infrastructure) as of March 2017; see
# https://github.com/coq/coq/pull/467 for some discussion.
sudo: required
# Until Ocaml becomes a language, we set a known one.
language: c
cache:
apt: true
directories:
- $HOME/.opam
before_cache:
- rm -rf ~/.opam/log/
addons:
apt:
sources:
- avsm
## Due to issues like
## https://github.com/travis-ci/travis-ci/issues/8507 ,
## https://github.com/travis-ci/travis-ci/issues/9000 ,
## https://github.com/travis-ci/travis-ci/issues/9081 , and
## https://github.com/travis-ci/travis-ci/issues/9126 , we get frequent
## failures with using `packages`. Therefore, for most targets, we
## instead invoke `apt-get update` manually with `travis_retry` before
## invoking `apt-get install`, manually, below in the `install:`
## target.
# packages:
# - opam
# - aspcud
# - gcc-multilib
env:
global:
- NJOBS=2
# system is == 4.02.3
- COMPILER="system"
- COMPILER_BE="4.07.0"
- DUNE_VER=".1.0.0"
- CAMLP5_VER=".6.14"
- CAMLP5_VER_BE=".7.06"
- FINDLIB_VER=".1.4.1"
- FINDLIB_VER_BE=".1.8.0"
- LABLGTK="lablgtk.2.18.3 conf-gtksourceview.2"
- LABLGTK_BE="lablgtk.2.18.6 conf-gtksourceview.2"
- NATIVE_COMP="yes"
- COQ_DEST="-local"
- MAIN_TARGET="world"
matrix:
include:
- if: NOT (type = pull_request)
env:
- TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="validate" TW="travis_wait"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="ci-coquelicot"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="ci-equations"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="ci-flocq"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="ci-hott"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="ci-ltac2"
- env:
- TEST_TARGET="lint"
install: []
before_script: []
addons:
apt:
sources: []
packages: []
script:
- dev/lint-repository.sh
# Full Coq test-suite with two compilers
- if: NOT (type = pull_request)
env:
- TEST_TARGET="sphinx test-suite"
- EXTRA_CONF="-coqide opt"
- EXTRA_OPAM="hevea ${LABLGTK}"
before_install: &sphinx-install
- sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex
addons:
apt:
sources:
- avsm
packages: &extra-packages
- opam
- aspcud
- libgtk2.0-dev
- libgtksourceview2.0-dev
- python3
- python3-pip
- python3-setuptools
- if: NOT (type = pull_request)
env:
- TEST_TARGET="sphinx test-suite"
- COMPILER="${COMPILER_BE}"
- FINDLIB_VER="${FINDLIB_VER_BE}"
- CAMLP5_VER="${CAMLP5_VER_BE}"
- EXTRA_CONF="-coqide opt"
- EXTRA_OPAM="hevea ${LABLGTK_BE}"
before_install: *sphinx-install
addons:
apt:
sources:
- avsm
packages: *extra-packages
# Full test-suite with flambda
- if: NOT (type = pull_request)
env:
- TEST_TARGET="sphinx test-suite"
- COMPILER="${COMPILER_BE}+flambda"
- FINDLIB_VER="${FINDLIB_VER_BE}"
- CAMLP5_VER="${CAMLP5_VER_BE}"
- EXTRA_CONF="-coqide opt -flambda-opts -O3"
- EXTRA_OPAM="hevea ${LABLGTK_BE}"
before_install: *sphinx-install
addons:
apt:
sources:
- avsm
packages: *extra-packages
- os: osx
env:
- TEST_TARGET="test-suite"
- COMPILER="${COMPILER_BE}"
- FINDLIB_VER="${FINDLIB_VER_BE}"
- CAMLP5_VER="${CAMLP5_VER_BE}"
- NATIVE_COMP="no"
- COQ_DEST="-local"
before_install:
- brew update
- brew unlink python
- brew install gnu-time
# only way to continue using OPAM 1.2
- brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb
- if: NOT (type = pull_request)
os: osx
osx_image: xcode7.3
env:
- TEST_TARGET=""
- COMPILER="${COMPILER_BE}"
- FINDLIB_VER="${FINDLIB_VER_BE}"
- CAMLP5_VER="${CAMLP5_VER_BE}"
- NATIVE_COMP="no"
- COQ_DEST="-prefix ${PWD}/_install"
- EXTRA_CONF="-coqide opt -warn-error yes"
- EXTRA_OPAM="${LABLGTK_BE}"
before_install:
- brew update
- brew unlink python
- brew install gnu-time gtk+ expat gtksourceview gdk-pixbuf
# only way to continue using OPAM 1.2
- brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb
- brew unlink python@2
- brew install python3
- pip3 install macpack
before_deploy:
- dev/build/osx/make-macos-dmg.sh
deploy:
- provider: bintray
user: maximedenes
file: .bintray.json
key:
secure: "gUvXWwWR0gicDqsKOnBfe45taToSFied6gN8tCa5IOtl6E6gFoHoPZ83ZWXQsZP50oMDFS5eji0VQAFGEbOsGrTZaD9Y9Jnu34NND78SWL1tsJ6nHO3aCAoMpB0N3+oRuF6S+9HStU6KXWqgj+GeU4vZ4TOlG01RGctJa6U3vII="
skip_cleanup: true
on:
all_branches: true
before_install:
- if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi
install:
- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then travis_retry ./dev/tools/sudo-apt-get-update.sh -q; fi
- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then sudo apt-get install -y opam aspcud gcc-multilib --allow-unauthenticated; fi
- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
- opam switch "$COMPILER" && opam update
- eval $(opam config env)
- opam config list
- opam install -j ${NJOBS} -y num ocamlfind${FINDLIB_VER} camlp5${CAMLP5_VER} ${EXTRA_OPAM}
- opam list
script:
- set -e
- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
- ./configure ${COQ_DEST} -warn-error yes -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
- echo -en 'travis_fold:end:coq.config\\r'
- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
- make -j ${NJOBS} ${MAIN_TARGET}
- echo -en 'travis_fold:end:coq.build\\r'
- echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
- if [ -n "${TEST_TARGET}" ]; then ${TW} make -j ${NJOBS} ${TEST_TARGET}; fi
- echo -en 'travis_fold:end:coq.test\\r'
- set +e
# Testing Gitter webhook
notifications:
webhooks:
urls:
- https://webhooks.gitter.im/e/3cdabdec318214c7cd63
on_success: change # options: [always|never|change] default: always
on_failure: always # options: [always|never|change] default: always
on_start: never # options: [always|never|change] default: always
CHANGES → CHANGES.md
View file @ a7783b2b
Changes from 8.9+beta1 to 8.9.0
===============================
Assorted bug fixes.
Changes from 8.8.2 to 8.9+beta1
===============================
Kernel
- Mutually defined records are now supported.
Notations
- New support for autonomous grammars of terms, called "custom
entries" (see chapter "Syntax extensions" of the reference manual).
- Deprecated compatibility notations will actually be removed in the
next version of Coq. Uses of these notations are generally easy to
fix thanks to the hint contained in the deprecation warnings. For
projects that require more than a handful of such fixes, there is [a
script](https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py)
that will do it automatically, using the output of coqc. The script
contains documentation on its usage in a comment at the top.
Tactics
- Added toplevel goal selector `!` which expects a single focused goal.
Use with `Set Default Goal Selector` to force focusing before tactics
are called.
- The undocumented "nameless" forms `fix N`, `cofix` that were
deprecated in 8.8 have been removed from Ltac's syntax; please use
`fix ident N/cofix ident` to explicitly name the (co)fixpoint
hypothesis to be introduced.
- Introduction tactics `intro`/`intros` on a goal that is an
existential variable now force a refinement of the goal into a
dependent product rather than failing.
- Support for `fix`/`cofix` added in Ltac `match` and `lazymatch`.
- Ltac backtraces now include trace information about tactics
called by OCaml-defined tactics.
- Option `Ltac Debug` now applies also to terms built using Ltac functions.
- Deprecated the `Implicit Tactic` family of commands.
- The default program obligation tactic uses a bounded proof search
instead of an unbounded and potentially non-terminating one now
(source of incompatibility).
- The `simple apply` tactic now respects the `Opaque` flag when called from
Ltac (`auto` still does not respect it).
- Tactic `constr_eq` now adds universe constraints needed for the
identity to the context (it used to ignore them). New tactic
`constr_eq_strict` checks that the required constraints already hold
without adding new ones. Preexisting tactic `constr_eq_nounivs` can
still be used if you really want to ignore universe constraints.
- Tactics and tactic notations now understand the `deprecated` attribute.
- The `fourier` tactic has been removed. Please now use `lra` instead. You
may need to add `Require Import Lra` to your developments. For compatibility,
we now define `fourier` as a deprecated alias of `lra`.
- The `romega` tactics have been deprecated; please use `lia` instead.
Focusing
- Focusing bracket `{` now supports named goal selectors,
e.g. `[x]: {` will focus on a goal (existential variable) named `x`.
As usual, unfocus with `}` once the sub-goal is fully solved.
Specification language
- A fix to unification (which was sensitive to the ascii name of
variables) may occasionally change type inference in incompatible
ways, especially regarding the inference of the return clause of `match`.
Standard Library
- Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,
and proved some lemmas about them. Note that this might cause
incompatibilities if you have, e.g., `string_scope` and `Z_scope` both
open with `string_scope` on top, and expect `=?` to refer to `Z.eqb`.
Solution: wrap `_ =? _` in `(_ =? _)%Z` (or whichever scope you
want).
- Added `Ndigits.N2Bv_sized`, and proved some lemmas about it.
Deprecated `Ndigits.N2Bv_gen`.
- The scopes `int_scope` and `uint_scope` have been renamed to
`dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect
and other packages. They are still delimited by `%int` and `%uint`.
- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`,
and `int31` are no longer available merely by `Require`ing the files
that define the inductives. You must `Import` `Coq.Strings.String`,
`Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
`Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and
`Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use
these notations. Note that passing `-compat 8.8` or issuing
`Require Import Coq.Compat.Coq88` will make these notations
available. Users wishing to port their developments automatically
may download `fix.py` from
<https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169>
and run a command like `while true; do make -Okj 2>&1 |
/path/to/fix.py; done` and get a cup of coffee. (This command must
be manually interrupted once the build finishes all the way though.
Note also that this method is not fail-proof; you may have to adjust
some scopes if you were relying on string notations not being
available even when `string_scope` was open.)
- Numeral syntax for `nat` is no longer available without loading the
entire prelude (`Require Import Coq.Init.Prelude`). This only
impacts users running Coq without the init library (`-nois` or
`-noinit`) and also issuing `Require Import Coq.Init.Datatypes`.
Tools
- Coq_makefile lets one override or extend the following variables from
the command line: `COQFLAGS`, `COQCHKFLAGS`, `COQDOCFLAGS`.
`COQFLAGS` is now entirely separate from `COQLIBS`, so in custom Makefiles
`$(COQFLAGS)` should be replaced by `$(COQFLAGS) $(COQLIBS)`.
- Removed the `gallina` utility (extracts specification from Coq vernacular files).
If you would like to maintain this tool externally, please contact us.
- Removed the Emacs modes distributed with Coq. You are advised to
use [Proof-General](https://proofgeneral.github.io/) (and optionally
[Company-Coq](https://github.com/cpitclaudel/company-coq)) instead.
If your use case is not covered by these alternative Emacs modes,
please open an issue. We can help set up external maintenance as part
of Proof-General, or independently as part of coq-community.
Vernacular Commands
- Removed deprecated commands `Arguments Scope` and `Implicit Arguments`
(not the option). Use the `Arguments` command instead.
- Nested proofs may be enabled through the option `Nested Proofs Allowed`.
By default, they are disabled and produce an error. The deprecation
warning which used to occur when using nested proofs has been removed.
- Added option `Uniform Inductive Parameters` which abstracts over parameters
before typechecking constructors, allowing to write for example
`Inductive list (A : Type) := nil : list | cons : A -> list -> list.`
- New `Set Hint Variables/Constants Opaque/Transparent` commands for setting
globally the opacity flag of variables and constants in hint databases,
overwritting the opacity set of the hint database.
- Added generic syntax for "attributes", as in:
`#[local] Lemma foo : bar.`
- Added the `Numeral Notation` command for registering decimal numeral
notations for custom types
- The `Set SsrHave NoTCResolution` command no longer has special global
scope. If you want the previous behavior, use `Global Set SsrHave
NoTCResolution`.
- Multiple sections with the same name are allowed.
Coq binaries and process model
- Before 8.9, Coq distributed a single `coqtop` binary and a set of
dynamically loadable plugins that used to take over the main loop
for tasks such as IDE language server or parallel proof checking.
These plugins have been turned into full-fledged binaries so each
different process has associated a particular binary now, in
particular `coqidetop` is the CoqIDE language server, and
`coq{proof,tactic,query}worker` are in charge of task-specific and
parallel proof checking.
SSReflect
- The implementation of delayed clear switches in intro patterns
is now simpler to explain:
1. The immediate effect of a clear switch like `{x}` is to rename the
variable `x` to `_x_` (i.e. a reserved identifier that cannot be mentioned
explicitly)
2. The delayed effect of `{x}` is that `_x_` is cleared at the end of the intro
pattern
3. A clear switch immediately before a view application like `{x}/v` is
translated to `/v{x}`.
In particular, the third rule lets one write `{x}/v` even if `v` uses the variable `x`:
indeed the view is executed before the renaming.
- An empty clear switch is now accepted in intro patterns before a
view application whenever the view is a variable.
One can now write `{}/v` to mean `{v}/v`. Remark that `{}/x` is very similar
to the idiom `{}e` for the rewrite tactic (the equation `e` is used for
rewriting and then discarded).
Standard Library
- There are now conversions between `string` and `positive`, `Z`,
`nat`, and `N` in binary, octal, and hex.
Display diffs between proof steps
- `coqtop` and `coqide` can now highlight the differences between proof steps
in color. This can be enabled from the command line or the
`Set Diffs "on"/"off"/"removed"` command. Please see the documentation for
details. Showing diffs in Proof General requires small changes to PG
(under discussion).
Notations
- Added `++` infix for `VectorDef.append`.
Note that this might cause incompatibilities if you have, e.g., `list_scope`
and `vector_scope` both open with `vector_scope` on top, and expect `++` to
refer to `app`.
Solution: wrap `_ ++ _` in `(_ ++ _)%list` (or whichever scope you want).
Changes from 8.8.1 to 8.8.2
===========================
......@@ -30,10 +243,10 @@ Changes from 8.8.0 to 8.8.1
Kernel
- Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333).
- Fix a critical bug with cofixpoints and `vm_compute`/`native_compute` (#7333).
- Fix a critical bug with modules and algebraic universes (#7695)
- Fix a critical bug with inlining of polymorphic constants (#7615).
- Fix a critical bug with universe polymorphism and vm_compute (#7723). Was
- Fix a critical bug with universe polymorphism and `vm_compute` (#7723). Was
present since 8.5.
Notations
......@@ -57,14 +270,14 @@ Changes from 8.8+beta1 to 8.8.0
Tools
- Asynchronous proof delegation policy was fixed. Since version 8.7
Coq was ignoring previous runs and the -async-proofs-delegation-threshold
Coq was ignoring previous runs and the `-async-proofs-delegation-threshold`
option did not have the expected behavior.
Tactic language
- The undocumented "nameless" forms `fix N`, `cofix N` have been
deprecated; please use `fix/cofix ident N` to explicitely name
hypothesis to be introduced.
- The undocumented "nameless" forms `fix N`, `cofix` have been
deprecated; please use `fix ident N /cofix ident` to explicitely
name the (co)fixpoint hypothesis to be introduced.
Documentation
......@@ -114,7 +327,7 @@ Tactics
profiling, and "Set NativeCompute Profile Filename" customizes
the profile filename.
- The tactic "omega" is now aware of the bodies of context variables
such as "x := 5 : Z" (see BZ#148). This could be disabled via
such as "x := 5 : Z" (see #1362). This could be disabled via
Unset Omega UseLocalDefs.
- The tactic "romega" is also aware now of the bodies of context variables.
- The tactic "zify" resp. "omega with N" is now aware of N.pred.
......@@ -299,7 +512,7 @@ Improvements around some error messages.
Many bug fixes including two important ones:
- BZ#5730: CoqIDE becomes unresponsive on file open.
- Bug #5730: CoqIDE becomes unresponsive on file open.
- coq_makefile: make sure compile flags for Coq and coq_makefile are in sync
(in particular, make sure the `-safe-string` option is used to compile plugins).
......@@ -349,7 +562,7 @@ Tactics
which behave like the corresponding variants with no "e" but turn
unresolved implicit arguments into existential variables, on the
shelf, rather than failing.
- Tactic injection has become more powerful (closes BZ#4890) and its
- Tactic injection has become more powerful (closes bug #4890) and its
documentation has been updated.
- New variants of the `first` and `solve` tacticals that do not rely
on parsing rules, meant to define tactic notations.
......@@ -395,7 +608,7 @@ Standard Library
file ChoiceFacts.v.
- New lemmas about iff and about orders on positive and Z.
- New lemmas on powerRZ.
- Strengthened statement of JMeq_eq_dep (closes BZ#4912).
- Strengthened statement of JMeq_eq_dep (closes bug #4912).
- The BigN, BigZ, BigZ libraries are no longer part of the Coq standard
library, they are now provided by a separate repository
https://github.com/coq/bignums
......@@ -470,12 +683,12 @@ XML Protocol and internal changes
See dev/doc/changes.txt
Many bugfixes including BZ#1859, BZ#2884, BZ#3613, BZ#3943, BZ#3994,
BZ#4250, BZ#4709, BZ#4720, BZ#4824, BZ#4844, BZ#4911, BZ#5026, BZ#5233,
BZ#5275, BZ#5315, BZ#5336, BZ#5360, BZ#5390, BZ#5414, BZ#5417, BZ#5420,
BZ#5439, BZ#5449, BZ#5475, BZ#5476, BZ#5482, BZ#5501, BZ#5507, BZ#5520,
BZ#5523, BZ#5524, BZ#5553, BZ#5577, BZ#5578, BZ#5589, BZ#5597, BZ#5598,
BZ#5607, BZ#5618, BZ#5619, BZ#5620, BZ#5641, BZ#5648, BZ#5651, BZ#5671.
Many bugfixes including #1859, #2884, #3613, #3943, #3994,
#4250, #4709, #4720, #4824, #4844, #4911, #5026, #5233,
#5275, #5315, #5336, #5360, #5390, #5414, #5417, #5420,
#5439, #5449, #5475, #5476, #5482, #5501, #5507, #5520,
#5523, #5524, #5553, #5577, #5578, #5589, #5597, #5598,
#5607, #5618, #5619, #5620, #5641, #5648, #5651, #5671.
Many bugfixes on OS X and Windows (now the test-suite passes on these
platforms too).
......@@ -2651,7 +2864,7 @@ Tactics
a registered setoid equality before starting to reduce in H. This is unlikely
to break any script. Should this happen nonetheless, one can insert manually
some "unfold ... in H" before rewriting.
- Fixed various bugs about (setoid) rewrite ... in ... (in particular BZ#1101)
- Fixed various bugs about (setoid) rewrite ... in ... (in particular bug #5941)
- "rewrite ... in" now accepts a clause as place where to rewrite instead of
juste a simple hypothesis name. For instance:
rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H
......@@ -3228,11 +3441,11 @@ Incompatibilities
Bugs
- Improved localisation of errors in Syntactic Definitions
- Induction principle creation failure in presence of let-in fixed (BZ#238)
- Inversion bugs fixed (BZ#212 and BZ#220)
- Omega bug related to Set fixed (BZ#180)
- Type-checking inefficiency of nested destructuring let-in fixed (BZ#216)
- Improved handling of let-in during holes resolution phase (BZ#239)
- Induction principle creation failure in presence of let-in fixed (#1459)
- Inversion bugs fixed (#1427 and #1437)
- Omega bug related to Set fixed (#1384)
- Type-checking inefficiency of nested destructuring let-in fixed (#1435)
- Improved handling of let-in during holes resolution phase (#1460)
Efficiency
......@@ -3245,18 +3458,18 @@ Changes from V7.3 to V7.3.1
Bug fixes
- Corrupted Field tactic and Match Context tactic construction fixed
- Checking of names already existing in Assert added (BZ#182)
- Invalid argument bug in Exact tactic solved (BZ#183)
- Colliding bound names bug fixed (BZ#202)
- Wrong non-recursivity test for Record fixed (BZ#189)
- Out of memory/seg fault bug related to parametric inductive fixed (BZ#195)
- Checking of names already existing in Assert added (#1386)
- Invalid argument bug in Exact tactic solved (#1387)
- Colliding bound names bug fixed (#1412)
- Wrong non-recursivity test for Record fixed (#1394)
- Out of memory/seg fault bug related to parametric inductive fixed (#1404)
- Setoid_replace/Setoid_rewrite bug wrt "==" fixed
Misc
- Ocaml version >= 3.06 is needed to compile Coq from sources
- Simplification of fresh names creation strategy for Assert, Pose and
LetTac (BZ#192)
LetTac (#1402)
Changes from V7.2 to V7.3
=========================
......
CONTRIBUTING.md
View file @ a7783b2b
......@@ -20,17 +20,38 @@ If you want to minimize your bug (or help minimize someone else's) for more extr
## Pull requests
**Beginner's guide to hacking Coq: [`dev/doc/README.md`](dev/doc/README.md)** \
**Development information and tools: [`dev/README.md`](dev/README.md)**
If you want to contribute a bug fix or feature yourself, pull requests on the [GitHub repository](https://github.com/coq/coq) are the way to contribute directly to the Coq implementation. We recommend you create a fork of the repository on GitHub and push your changes to a new "topic branch" in that fork. From there you can follow the [GitHub pull request documentation](https://help.github.com/articles/about-pull-requests/) to get your changes reviewed and pulled into the Coq source repository.
Documentation for getting started with the Coq sources is located in various files in [`dev/doc`](/dev/doc) (for example, [debugging.md](/dev/doc/debugging.md)). For further help with the Coq sources, feel free to join the [Coq Gitter chat](https://gitter.im/coq/coq) and ask questions.
Documentation for getting started with the Coq sources is located in various
files in [`dev/doc`](dev/doc) (for example, [debugging.md](dev/doc/debugging.md)).
For further help with the Coq sources, feel free to join
the [Coq Gitter chat](https://gitter.im/coq/coq) and ask questions.
Please make pull requests against the `master` branch.
If it's your first significant contribution to Coq (significant means: more than fixing a typo), your pull request should include a commit adding your name to the [`CREDITS`](/CREDITS) file (possibly with the name of your institution / employer if relevant to your contribution, an ORCID if you have one —you may log into https://orcid.org/ using your institutional account to get one—, and the year of your contribution).
If it's your first significant contribution to Coq (significant means: more
than fixing a typo), your pull request should include a commit adding your name
to the [`CREDITS`](CREDITS) file (possibly with the name of your
institution / employer if relevant to your contribution, an ORCID if you have
one —you may log into https://orcid.org/ using your institutional account to
get one—, and the year of your contribution).
It's helpful to run the Coq test suite with `make test-suite` before submitting
your change. Our CI runs this test suite and lots of other tests, including
building external Coq developments, on every pull request, but these results
take significantly longer to come back (on the order of a few hours). Running
the test suite locally will take somewhere around 10-15 minutes. Refer to
[`dev/ci/README.md`](dev/ci/README.md#information-for-developers) for more
information on CI tests, including how to run them on your private branches.
It's helpful to run the Coq test suite with `make test-suite` before submitting your change. Travis CI runs this test suite and a much larger one including external Coq developments on every pull request, but these results take significantly longer to come back (on the order of a few hours). Running the test suite locally will take somewhere around 10-15 minutes. Refer to [`dev/ci/README.md`](/dev/ci/README.md#information-for-developers) for more information on Travis CI tests.
If your pull request fixes a bug, please consider adding a regression test as
well. See [`test-suite/README.md`](test-suite/README.md) for how to do so.
If your pull request fixes a bug, please consider adding a regression test as well. See [`test-suite/README.md`](/test-suite/README.md) for how to do so.
If your pull request fixes a critical bug (a bug allowing a proof of `False`),
please add an entry to [`dev/doc/critical-bugs`](/dev/doc/critical-bugs).
Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes.
......@@ -38,13 +59,22 @@ Whitespace discipline (do not indent using tabs, no trailing spaces, text files
Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests.
- [needs: rebase](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22%20) indicates the PR should be rebased on top of the latest `master` branch. See the [GitHub documentation](https://help.github.com/articles/about-git-rebase/) for a brief introduction to using `git rebase`.
- [needs: fixing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22) indicates the PR needs a fix, as discussed in the comments.
- [needs: testing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22) indicates the PR needs testing. This is often used when testing beyond what the test suite can handle is required. For example, performance benchmarking is currently performed with a different infrastructure. Unless some followup is specifically requested you aren't expected to do this additional testing.
The release manager uses the following filter to know which PRs seem ready for merge. If you are waiting for a PR to be merged, make sure it appears in this list:
- [Pull requests ready for merge](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Apr%20is%3Aopen%20-label%3A%22needs%3A%20discussion%22%20-label%3A%22needs%3A%20testing%22%20-label%3A%22needs%3A%20fixing%22%20-label%3A%22needs%3A%20progress%22%20-label%3A%22needs%3A%20rebase%22%20-label%3A%22needs%3A%20review%22%20-label%3A%22needs%3A%20help%22%20-label%3A%22needs%3A%20independent%20fix%22%20-label%3A%22needs%3A%20feedback%22%20-label%3A%22help%20wanted%22%20-review%3Achanges_requested%20-status%3Apending%20base%3Amaster%20sort%3Aupdated-asc%20-label%3A%22needs%3A%20squashing%22%20)
- [needs: rebase][rebase-label] indicates the PR should be rebased on top of
the latest base branch (usually `master`). See the
[GitHub documentation](https://help.github.com/articles/about-git-rebase/)
for a brief introduction to using `git rebase`.
This label will be automatically added if you open or synchronize your PR and
it is not up-to-date with the base branch. So please, do not forget to rebase
your branch every time you update it.
- [needs: fixing][fixing-label] indicates the PR needs a fix, as discussed in the comments.
- [needs: benchmarking][benchmarking-label] and [needs: testing][testing-label]
indicate the PR needs testing beyond what the test suite can handle.
For example, performance benchmarking is currently performed with a different
infrastructure ([documented in the wiki][jenkins-doc]). Unless some followup
is specifically requested you aren't expected to do this additional testing.
To learn more about the merging process, you can read the
[merging documentation for Coq maintainers](dev/doc/MERGING.md).
## Documentation
......@@ -52,10 +82,24 @@ Currently the process for contributing to the documentation is the same as for c
Our issue tracker includes a flag to mark bugs related to documentation. You can view a list of documentation-related bugs using a [GitHub issue search](https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22). Many of these bugs can be fixed by contributing writing, without knowledge of Coq's OCaml source code.
The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) are at [`doc/refman`](/doc/refman). These are written in LaTeX and compiled to HTML with [HeVeA](http://hevea.inria.fr/).
The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) are at [`doc/sphinx`](/doc/sphinx). These are written in reStructuredText and compiled to HTML and PDF with [Sphinx](http://www.sphinx-doc.org/).
You may also contribute to the informal documentation available in [Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki), and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ). Both of these are editable by anyone with a GitHub account.
## Following the development
If you want to follow the development activity around Coq, you are encouraged
to subscribe to the [Coqdev mailing list](https://sympa.inria.fr/sympa/info/coqdev).
This mailing list has reasonably low traffic.
You may also choose to use GitHub feature to
["watch" this repository](https://github.com/coq/coq/subscription), but be
advised that this means receiving a very large number of notifications.
GitHub gives [some advice](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive)
on how to configure your e-mail client to filter these notifications.
A possible alternative is to deactivate e-mail notifications and manage your
GitHub web notifications using a tool such as [Octobox](http://octobox.io/).
## Contributing outside this repository
There are many useful ways to contribute to the Coq ecosystem that don't involve the Coq repository.
......@@ -67,3 +111,10 @@ External plugins / libraries contribute to create a successful ecosystem around
Ask and answer questions on [Stack Exchange](https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites) which has a helpful community of Coq users.
Hang out on the Coq IRC channel, `irc://irc.freenode.net/#coq`, and help answer questions.
[rebase-label]: https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22
[fixing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22
[benchmarking-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+benchmarking%22
[testing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22
[jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking)
CREDITS
View file @ a7783b2b
......@@ -37,8 +37,6 @@ plugins/extraction
developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now)
plugins/firstorder
developed by Pierre Corbineau (LRI, 2003-2008)
plugins/fourier
developed by Loïc Pottier (INRIA-Lemme, 2001)
plugins/funind
developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2006-now),
Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008, ENSIIE, 2008-now)
......@@ -128,6 +126,8 @@ of the Coq Proof assistant during the indicated time:
Matej Košík (INRIA, 2015-2017)
Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008,
INRIA-PPS then IRIF, 2009-now)
Yishuai Li (ORCID: https://orcid.org/0000-0002-5728-5903
U. Penn, 2018)
Patrick Loiseleur (Paris Sud, 1997-1999)
Evgeny Makarov (INRIA, 2007)
Gregory Malecha (Harvard University 2013-2015,
......
INSTALL
View file @ a7783b2b
......@@ -46,8 +46,8 @@ WHAT DO YOU NEED ?
- a C compiler
- for Coqide, the Lablgtk development files, and the GTK libraries
including gtksourceview, see INSTALL.ide for more details
- for CoqIDE, the lablgtk development files (version >= 2.18.3),
and the GTK 2.x libraries including gtksourceview2.
Note that num, camlp5 and lablgtk should be properly registered with
findlib/ocamlfind as Coq's makefile will use it to locate the
......
INSTALL.doc deleted 100644 → 0
View file @ 11d2b496
The Coq documentation
=====================
The Coq documentation includes
- A Reference Manual
- A Tutorial
- A document presenting the Coq standard library
- A list of questions/answers in the FAQ style
The sources of the documents are mainly made of LaTeX code from which
user-readable PostScript or PDF files, or a user-browsable bunch of
html files are generated.
Prerequisite
------------
To produce all the documents, the following tools are needed:
- latex (latex2e)
- pdflatex
- dvips
- bibtex
- makeindex
- hevea
- Python 3
- Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/)
- sphinx_rtd_theme
- pexpect
- beautifulsoup4
- Antlr4 runtime for Python 3
Under recent Debian based operating systems (Debian 10 "Buster",
Ubuntu 18.04, ...) a working set of packages for compiling the
documentation for Coq is:
texlive-latex-extra texlive-fonts-recommended hevea python3-sphinx
python3-pexpect python3-sphinx-rtd-theme python3-bs4
python3-sphinxcontrib.bibtex python3-pip
Then, install the Python3 Antlr4 package:
pip3 install antlr4-python3-runtime
Nix users should get the correct development environment to build the
Sphinx documentation from Coq's `default.nix`. [Note Nix setup doesn't
include the LaTeX packages needed to build the full documentation.]
If you are in an older/different distribution you can install the
Python packages required to build the user manual using python3-pip:
pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex
Compilation
-----------
To produce all documentation about Coq, just run:
./configure (if you hadn't already)
make doc
Alternatively, you can use some specific targets:
make doc-ps
to produce all PostScript documents
make doc-pdf
to produce all PDF documents
make doc-html
to produce all html documents
make sphinx
to produce the HTML version of the reference manual
make tutorial
to produce all formats of the tutorial
make rectutorial
to produce all formats of the tutorial on recursive types
make faq
to produce all formats of the FAQ
make stdlib
to produce all formats of the Coq standard library
Also note the "-with-doc yes" option of ./configure to enable the
build of the documentation as part of the default make target.
Installation
------------
To install all produced documents, do:
make DOCDIR=/some/directory/for/documentation install-doc
DOCDIR defauts to /usr/share/doc/coq
INSTALL.ide deleted 100644 → 0
View file @ 11d2b496
CoqIde Installation procedure
CoqIde is a graphical interface to perform interactive proofs.
You should be able to do everything you do in coqtop inside CoqIde
excepted dropping to the ML toplevel.
DISTRIBUTION PACKAGES
Your POSIX operating system may already contain precompiled packages
for Coq, including CoqIde, or a ready-to-compile... If the version
provided there suits you, follow the usual procedure for your
operating system.
E.g., on Debian GNU/Linux (or Debian GNU/k*BSD or ...), do:
aptitude install coqide
On Gentoo GNU/Linux, do:
USE=ide emerge sci-mathematics/coq
Else, read the rest of this document to compile your own CoqIde.
COMPILATION REQUIREMENTS
- OCaml >= 4.02.3 with native threads support.
- make world must succeed.
- The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
The official supported version is at least 2.24.x.
You may still compile CoqIde with older versions and use all features.
Run
pkg-config --modversion gtk+-2.0
to check your version.
Do not forget to install the development headers packages.
On Debian, installing lablgtk2 (see below) will automatically
install GTK+. (But "aptitude install libgtk2.0-dev" will
install GTK+ 2.x, should you need to force it for one reason
or another.)
- The OCaml bindings for GTK+ 2.x, lablgtk2 with support for gtksourceview2.
You need at least version 2.18.3.
Your distribution may contain precompiled packages. For example, for
Debian, run
aptitude install liblablgtksourceview2-ocaml-dev
for Mandriva, run
urpmi ocaml-lablgtk-devel
If it does not, see http://lablgtk.forge.ocamlcore.org/
The basic command installing lablgtk2 from the source package is:
./configure && make world && make install
You must have write access to the OCaml standard library path.
If this fails, read the README.
INSTALLATION
0) For optimal performance, OCaml must support native threads (aka pthreads).
If this not the case, this means that Coq computations will be slow and
"make ide" will fail. Use "make bin/coqide.byte" instead. To fix this
problem, just recompile OCaml from source and configure OCaml with:
"./configure --with-pthreads".
In case you install over an existing copy of OCaml, you should better
empty the OCaml installation directory.
1) Go into your Coq source directory and, as usual, configure with:
./configure
This should detect the ability of making CoqIde; check in the
report printed by configure that ability to build CoqIde is detected.
Then compile with
make world
and install with
make install
In case you are upgrading from an old version you may need to run
make clean-ide
2) You may now run bin/coqide
NOTES
There are three configuration files located in your $(XDG_CONFIG_HOME)/coq
dir (defaulting to $HOME/.config/coq).
- coqiderc is generated by coqide itself. It may be edited by hand or
by using the Preference menu from coqide. It will be generated the first time
you save your the preferences in Coqide.
- coqide.keys is a standard Gtk2 accelerator dump. You may edit this file
to change the default shortcuts for the menus.
Read ide/FAQ for more informations.
TROUBLESHOOTING
- Problem with automatic templates
Some users may experiment problems with unwanted automatic
templates while using Coqide. This is due to a change in the
modifiers keys available through GTK. The straightest way to get
rid of the problem is to edit by hand your coqiderc (either
/home/<user>/.config/coq/coqiderc under Linux, or
C:\Documents and Settings\<user>\.config\coq\coqiderc under Windows)
and replace any occurrence of MOD4 by MOD1.
META.coq → META.coq.in
View file @ a7783b2b
# TODO: Generate automatically with Dune
description = "The Coq Proof Assistant Plugin API"
version = "8.8"
version = "8.9"
directory = ""
requires = "camlp5"
package "grammar" (
description = "Coq Camlp5 Grammar Extensions for Plugins"
version = "8.9"
requires = "camlp5.gramlib"
directory = "grammar"
archive(byte) = "grammar.cma"
archive(native) = "grammar.cmxa"
)
package "config" (
description = "Coq Configuration Variables"
version = "8.8"
version = "8.9"
directory = "config"
......@@ -17,7 +29,7 @@ package "config" (
package "clib" (
description = "Base General Coq Library"
version = "8.8"
version = "8.9"
directory = "clib"
requires = "num, str, unix, threads"
......@@ -29,7 +41,7 @@ package "clib" (
package "lib" (
description = "Base Coq-Specific Library"
version = "8.8"
version = "8.9"
directory = "lib"
......@@ -43,7 +55,7 @@ package "lib" (
package "vm" (
description = "Coq VM"
version = "8.8"
version = "8.9"
directory = "kernel/byterun"
......@@ -57,15 +69,12 @@ package "vm" (
# We currently prefer static linking of the VM.
archive(byte) = "libcoqrun.a"
linkopts(byte) = "-custom"
linkopts(native) = "-cclib -lcoqrun"
)
package "kernel" (
description = "Coq's Kernel"
version = "8.8"
version = "8.9"
directory = "kernel"
......@@ -79,7 +88,7 @@ package "kernel" (
package "library" (
description = "Coq Libraries (vo) support"
version = "8.8"
version = "8.9"
requires = "coq.kernel"
......@@ -90,23 +99,10 @@ package "library" (
)
package "intf" (
description = "Coq Public Data Types"
version = "8.8"
requires = "coq.library"
directory = "intf"
archive(byte) = "intf.cma"
archive(native) = "intf.cmxa"
)
package "engine" (
description = "Coq Tactic Engine"
version = "8.8"
version = "8.9"
requires = "coq.library"
directory = "engine"
......@@ -119,7 +115,7 @@ package "engine" (
package "pretyping" (
description = "Coq Pretyper"
version = "8.8"
version = "8.9"
requires = "coq.engine"
directory = "pretyping"
......@@ -132,7 +128,7 @@ package "pretyping" (
package "interp" (
description = "Coq Term Interpretation"
version = "8.8"
version = "8.9"
requires = "coq.pretyping"
directory = "interp"
......@@ -142,22 +138,10 @@ package "interp" (
)
package "grammar" (
description = "Coq Base Grammar"
version = "8.8"
requires = "coq.interp"
directory = "grammar"
archive(byte) = "grammar.cma"
archive(native) = "grammar.cmxa"
)
package "proofs" (
description = "Coq Proof Engine"
version = "8.8"
version = "8.9"
requires = "coq.interp"
directory = "proofs"
......@@ -170,7 +154,7 @@ package "proofs" (
package "parsing" (
description = "Coq Parsing Engine"
version = "8.8"
version = "8.9"
requires = "camlp5.gramlib, coq.proofs"
directory = "parsing"
......@@ -183,7 +167,7 @@ package "parsing" (
package "printing" (
description = "Coq Printing Engine"
version = "8.8"
version = "8.9"
requires = "coq.parsing"
directory = "printing"
......@@ -196,7 +180,7 @@ package "printing" (
package "tactics" (
description = "Coq Basic Tactics"
version = "8.8"
version = "8.9"
requires = "coq.printing"
directory = "tactics"
......@@ -209,7 +193,7 @@ package "tactics" (
package "vernac" (
description = "Coq Vernacular Interpreter"
version = "8.8"
version = "8.9"
requires = "coq.tactics"
directory = "vernac"
......@@ -222,7 +206,7 @@ package "vernac" (
package "stm" (
description = "Coq State Transactional Machine"
version = "8.8"
version = "8.9"
requires = "coq.vernac"
directory = "stm"
......@@ -235,7 +219,7 @@ package "stm" (
package "toplevel" (
description = "Coq Toplevel"
version = "8.8"
version = "8.9"
requires = "coq.stm"
directory = "toplevel"
......@@ -248,7 +232,7 @@ package "toplevel" (
package "idetop" (
description = "Coq IDE Libraries"
version = "8.8"
version = "8.9"
requires = "coq.toplevel"
directory = "ide"
......@@ -262,7 +246,7 @@ package "idetop" (
package "ide" (
description = "Coq IDE Libraries"
version = "8.8"
version = "8.9"
# XXX Add GTK
requires = "coq.toplevel"
......@@ -276,14 +260,14 @@ package "ide" (
package "plugins" (
description = "Coq built-in plugins"
version = "8.8"
version = "8.9"
directory = "plugins"
package "ltac" (
description = "Coq LTAC Plugin"
version = "8.8"
version = "8.9"
requires = "coq.stm"
directory = "ltac"
......@@ -296,7 +280,7 @@ package "plugins" (
package "tauto" (
description = "Coq tauto plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.ltac"
directory = "ltac"
......@@ -308,7 +292,7 @@ package "plugins" (
package "omega" (
description = "Coq omega plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.ltac"
directory = "omega"
......@@ -320,7 +304,7 @@ package "plugins" (
package "romega" (
description = "Coq romega plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.omega"
directory = "romega"
......@@ -332,7 +316,7 @@ package "plugins" (
package "micromega" (
description = "Coq micromega plugin"
version = "8.8"
version = "8.9"
requires = "num,coq.plugins.ltac"
directory = "micromega"
......@@ -344,7 +328,7 @@ package "plugins" (
package "quote" (
description = "Coq quote plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.ltac"
directory = "quote"
......@@ -356,7 +340,7 @@ package "plugins" (
package "newring" (
description = "Coq newring plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.quote"
directory = "setoid_ring"
......@@ -365,22 +349,10 @@ package "plugins" (
archive(native) = "newring_plugin.cmx"
)
package "fourier" (
description = "Coq fourier plugin"
version = "8.8"
requires = "coq.plugins.ltac"
directory = "fourier"
archive(byte) = "fourier_plugin.cmo"
archive(native) = "fourier_plugin.cmx"
)
package "extraction" (
description = "Coq extraction plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.ltac"
directory = "extraction"
......@@ -392,7 +364,7 @@ package "plugins" (
package "cc" (
description = "Coq cc plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.ltac"
directory = "cc"
......@@ -404,7 +376,7 @@ package "plugins" (
package "ground" (
description = "Coq ground plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.ltac"
directory = "firstorder"
......@@ -416,7 +388,7 @@ package "plugins" (
package "rtauto" (
description = "Coq rtauto plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.ltac"
directory = "rtauto"
......@@ -428,7 +400,7 @@ package "plugins" (
package "btauto" (
description = "Coq btauto plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.ltac"
directory = "btauto"
......@@ -440,7 +412,7 @@ package "plugins" (
package "recdef" (
description = "Coq recdef plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.extraction"
directory = "funind"
......@@ -452,7 +424,7 @@ package "plugins" (
package "nsatz" (
description = "Coq nsatz plugin"
version = "8.8"
version = "8.9"
requires = "num,coq.plugins.ltac"
directory = "nsatz"
......@@ -464,7 +436,7 @@ package "plugins" (
package "natsyntax" (
description = "Coq natsyntax plugin"
version = "8.8"
version = "8.9"
requires = ""
directory = "syntax"
......@@ -476,7 +448,7 @@ package "plugins" (
package "zsyntax" (
description = "Coq zsyntax plugin"
version = "8.8"
version = "8.9"
requires = ""
directory = "syntax"
......@@ -488,7 +460,7 @@ package "plugins" (
package "rsyntax" (
description = "Coq rsyntax plugin"
version = "8.8"
version = "8.9"
requires = ""
directory = "syntax"
......@@ -500,7 +472,7 @@ package "plugins" (
package "int31syntax" (
description = "Coq int31syntax plugin"
version = "8.8"
version = "8.9"
requires = ""
directory = "syntax"
......@@ -512,7 +484,7 @@ package "plugins" (
package "asciisyntax" (
description = "Coq asciisyntax plugin"
version = "8.8"
version = "8.9"
requires = ""
directory = "syntax"
......@@ -524,7 +496,7 @@ package "plugins" (
package "stringsyntax" (
description = "Coq stringsyntax plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.asciisyntax"
directory = "syntax"
......@@ -536,7 +508,7 @@ package "plugins" (
package "derive" (
description = "Coq derive plugin"
version = "8.8"
version = "8.9"
requires = ""
directory = "derive"
......@@ -548,7 +520,7 @@ package "plugins" (
package "ssrmatching" (
description = "Coq ssrmatching plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.ltac"
directory = "ssrmatching"
......@@ -560,7 +532,7 @@ package "plugins" (
package "ssreflect" (
description = "Coq ssreflect plugin"
version = "8.8"
version = "8.9"
requires = "coq.plugins.ssrmatching"
directory = "ssr"
......
Makefile
View file @ a7783b2b
......@@ -58,7 +58,7 @@ FIND_SKIP_DIRS:='(' \
-name '_build_ci' -o \
-name '_install_ci' -o \
-name 'user-contrib' -o \
-name 'coq-makefile' -o \
-name 'test-suite' -o \
-name '.opamcache' -o \
-name '.coq-native' \
')' -prune -o
......@@ -74,11 +74,15 @@ endef
## Files in the source tree
LEXFILES := $(call find, '*.mll')
YACCFILES := $(call find, '*.mly')
export MLLIBFILES := $(call find, '*.mllib')
export MLPACKFILES := $(call find, '*.mlpack')
export ML4FILES := $(call find, '*.ml4')
export MLGFILES := $(call find, '*.mlg')
export CFILES := $(call findindir, 'kernel/byterun', '*.c')
export MERLINFILES := $(call find, '.merlin')
MERLININFILES := $(call find, '.merlin.in')
export MERLINFILES := $(MERLININFILES:.in=)
# NB: The lists of currently existing .ml and .mli files will change
# before and after a build or a make clean. Hence we do not export
......@@ -90,7 +94,8 @@ EXISTINGMLI := $(call find, '*.mli')
## Files that will be generated
GENML4FILES:= $(ML4FILES:.ml4=.ml)
export GENMLFILES:=$(LEXFILES:.mll=.ml) kernel/copcodes.ml
GENMLGFILES:= $(MLGFILES:.mlg=.ml)
export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) kernel/copcodes.ml
export GENHFILES:=kernel/byterun/coq_jumptbl.h
export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
......@@ -100,7 +105,7 @@ export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
## More complex file lists
export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES), $(EXISTINGML))
export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES) $(GENMLGFILES), $(EXISTINGML))
export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
include Makefile.common
......@@ -111,7 +116,7 @@ include Makefile.common
NOARG: world
.PHONY: NOARG help noconfig submake
.PHONY: NOARG help noconfig submake camldevfiles
help:
@echo "Please use either:"
......@@ -138,46 +143,13 @@ Then, you may want to consider whether you want to restore the autosaves)
#run.
endif
# Check that every compiled file around has a known source file.
# This should help preventing weird compilation failures caused by leftover
# compiled files after deleting or moving some source files.
EXISTINGVO:=$(call find, '*.vo')
KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v'))
ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO))
EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa')
KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \
$(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp))
KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \
$(MLIFILES:.mli=.cmi) \
$(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma
ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS))
ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii
ifndef ACCEPT_ALIEN_VO
ifdef ALIENVO
$(error Leftover compiled Coq files without known sources: $(ALIENVO); \
remove them first, for instance via 'make voclean' or 'make alienclean' \
(or skip this check via 'make ACCEPT_ALIEN_VO=1'))
endif
endif
ifndef ACCEPT_ALIEN_OBJ
ifdef ALIENOBJS
$(error Leftover compiled OCaml files without known sources: $(ALIENOBJS); \
remove them first, for instance via 'make clean' or 'make alienclean' \
(or skip this check via 'make ACCEPT_ALIEN_OBJ=1'))
endif
endif
endif
# Apart from clean and tags, everything will be done in a sub-call to make
# on Makefile.build. This way, we avoid doing here the -include of .d :
# since they trigger some compilations, we do not want them for a mere clean.
# Moreover, we regroup this sub-call in a common target named 'submake'.
# This way, multiple user-given goals (cf the MAKECMDGOALS variable) won't
# trigger multiple (possibly parallel) make sub-calls
# Apart from clean and a few misc files, everything will be done in a
# sub-call to make on Makefile.build. This way, we avoid doing here
# the -include of .d : since they trigger some compilations, we do not
# want them for a mere clean. Moreover, we regroup this sub-call in a
# common target named 'submake'. This way, multiple user-given goals
# (cf the MAKECMDGOALS variable) won't trigger multiple (possibly
# parallel) make sub-calls
ifdef COQ_CONFIGURED
%:: submake ;
......@@ -187,7 +159,10 @@ endif
MAKE_OPTS := --warn-undefined-variable --no-builtin-rules
submake:
bin:
mkdir bin
submake: alienclean camldevfiles | bin
$(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS)
noconfig:
......@@ -197,13 +172,30 @@ noconfig:
Makefile $(wildcard Makefile.*) config/Makefile : ;
###########################################################################
# OCaml dev files
###########################################################################
camldevfiles: $(MERLINFILES) META.coq
# prevent submake dependency
META.coq.in $(MERLININFILES): ;
.merlin: .merlin.in
cp -a "$<" "$@"
%/.merlin: %/.merlin.in
cp -a "$<" "$@"
META.coq: META.coq.in
cp -a "$<" "$@"
###########################################################################
# Cleaning
###########################################################################
.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean alienclean
clean: objclean cruftclean depclean docclean devdocclean
clean: objclean cruftclean depclean docclean devdocclean camldevfilesclean
cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean devdocclean
......@@ -213,14 +205,16 @@ cruftclean: ml4clean
find . -name '*~' -o -name '*.annot' | xargs rm -f
rm -f gmon.out core
camldevfilesclean:
rm -f $(MERLINFILES) META.coq
indepclean:
rm -f $(GENFILES)
rm -f $(COQTOPBYTE) $(CHICKENBYTE)
rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE)
find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -delete
rm -f */*.pp[iox] plugins/*/*.pp[iox]
rm -rf $(SOURCEDOCDIR)
rm -f toplevel/mltop.byteml toplevel/mltop.optml
rm -f test-suite/check.log
rm -f glob.dump
rm -f config/revision.ml revision
rm -f plugins/micromega/.micromega.ml.generated
......@@ -246,7 +240,7 @@ archclean: clean-ide optclean voclean
rm -f $(ALLSTDLIB).*
optclean:
rm -f $(COQTOPEXE) $(CHICKEN)
rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT)
rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT)
find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
......@@ -258,7 +252,7 @@ clean-ide:
rm -rf $(COQIDEAPP)
ml4clean:
rm -f $(GENML4FILES)
rm -f $(GENML4FILES) $(GENMLGFILES)
depclean:
find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -print | xargs rm -f
......@@ -284,6 +278,22 @@ devdocclean:
rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex
rm -f $(OCAMLDOCDIR)/html/*.html
# Ensure that every compiled file around has a known source file.
# This should help preventing weird compilation failures caused by leftover
# compiled files after deleting or moving some source files.
EXISTINGVO:=$(call find, '*.vo')
KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v'))
ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO))
EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa')
KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \
$(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp))
KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \
$(MLIFILES:.mli=.cmi) \
$(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma
ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS))
alienclean:
rm -f $(ALIENOBJS) $(ALIENVO)
......
Makefile.build
View file @ a7783b2b
......@@ -89,6 +89,7 @@ byte: coqbyte coqide-byte pluginsbyte printers
MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
include Makefile.common
include Makefile.vofiles
include Makefile.doc ## provides the 'documentation' rule
include Makefile.checker
include Makefile.ide ## provides the 'coqide' rule
......@@ -194,7 +195,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
# the output format of the unix command time. For instance:
# TIME="%C (%U user, %S sys, %e total, %M maxres)"
COQOPTS=$(NATIVECOMPUTE)
COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR)
BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))
......@@ -205,15 +206,23 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS)
DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/utils)
DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/protocol)
# On MacOS, the binaries are signed, except our private ones
ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin)
LINKMETADATA=$(if $(filter $(PRIVATEBINARIES),$@),,-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist")
CODESIGN=$(if $(filter $(PRIVATEBINARIES),$@),true,codesign -s -)
CODESIGN_HIDE=$(CODESIGN)
else
LINKMETADATA=
CODESIGN=true
CODESIGN_HIDE=$(HIDE)true
endif
ifeq ($(STRIP),true)
STRIP_HIDE=$(HIDE)true
else
STRIP_HIDE=$(STRIP)
endif
# Best OCaml compiler, used in a generic way
......@@ -240,6 +249,10 @@ $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ -linkpkg $(1) $^ &&
$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^)
endef
define ocamlbyte
$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^
endef
# Camlp5 settings
CAMLP5DEPS:=grammar/grammar.cma
......@@ -337,6 +350,7 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
GRAMBASEDEPS := grammar/q_util.cmi
GRAMCMO := grammar/q_util.cmo \
grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo
COQPPCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex))
grammar/argextend.cmo : $(GRAMBASEDEPS)
grammar/q_util.cmo : $(GRAMBASEDEPS)
......@@ -344,6 +358,10 @@ grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo
grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \
grammar/argextend.cmo
coqpp/coqpp_parse.cmi: coqpp/coqpp_ast.cmi
coqpp/coqpp_parse.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmi
coqpp/coqpp_lex.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmo
## Ocaml compiler with the right options and -I for grammar
GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \
......@@ -354,11 +372,15 @@ GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \
grammar/grammar.cma : $(GRAMCMO)
$(SHOW)'Testing $@'
@touch grammar/test.mlp
$(HIDE)$(GRAMC) -pp '$(CAMLP5O) -I $(MYCAMLP5LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test
$(HIDE)$(GRAMC) -pp '$(CAMLP5O) $^ -impl' -impl grammar/test.mlp -o grammar/test
@rm -f grammar/test.* grammar/test
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(GRAMC) $^ -linkall -a -o $@
$(COQPP): $(COQPPCMO) coqpp/coqpp_main.ml
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(GRAMC) -I coqpp $^ -linkall -o $@
## Support of Camlp5 and Camlp5
COMPATCMO:=
......@@ -371,6 +393,10 @@ grammar/%.cmo: grammar/%.mlp | $(COMPATCMO)
$(SHOW)'OCAMLC -c -pp $<'
$(HIDE)$(GRAMC) -c -pp '$(GRAMPP)' -impl $<
grammar/%.cmo: grammar/%.ml | $(COMPATCMO)
$(SHOW)'OCAMLC -c -pp $<'
$(HIDE)$(GRAMC) -c $<
grammar/%.cmi: grammar/%.mli
$(SHOW)'OCAMLC -c $<'
$(HIDE)$(GRAMC) -c $<
......@@ -382,29 +408,34 @@ grammar/%.cmi: grammar/%.mli
.PHONY: coqbinaries coqbyte
coqbinaries: $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
coqbyte: $(TOPBYTE) $(CHICKENBYTE)
coqbyte: $(COQTOPBYTE) $(CHICKENBYTE)
# Special rule for coqtop, we imitate `ocamlopt` can delete the target
# to avoid #7666
$(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST))
rm -f $@ && cp $< $@
COQTOP_OPT=toplevel/coqtop_opt_bin.ml
COQTOP_BYTE=toplevel/coqtop_byte_bin.ml
bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \
$(SYSMOD) -package camlp5.gramlib \
$(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
$(STRIP_HIDE) $@
$(CODESIGN_HIDE) $@
ifeq ($(BEST),opt)
$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT)
bin/%.byte$(EXE): topbin/%_bin.ml $(LINKCMO) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(OCAMLOPT) -linkall -linkpkg -I vernac -I toplevel \
-I kernel/byterun/ -cclib -lcoqrun \
$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) \
-I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
$(SYSMOD) -package camlp5.gramlib \
$(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $(COQTOP_OPT) -o $@
$(STRIP) $@
$(CODESIGN) $@
else
$(COQTOPEXE): $(COQTOPBYTE)
cp $< $@
endif
$(LINKCMO) $(BYTEFLAGS) $< -o $@
COQTOP_BYTE=topbin/coqtop_byte_bin.ml
# Special rule for coqtop.byte
# VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM
$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE)
$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \
-I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
......@@ -418,6 +449,10 @@ $(COQC): $(call bestobj, $(COQCCMO))
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, $(SYSMOD))
$(COQCBYTE): $(COQCCMO)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(call ocamlbyte, $(SYSMOD))
###########################################################################
# other tools
###########################################################################
......@@ -455,10 +490,18 @@ $(COQDEPBOOT): $(call bestobj, $(COQDEPBOOTSRC))
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, -I tools -package unix)
$(COQDEPBOOTBYTE): $(COQDEPBOOTSRC)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(call ocamlbyte, -I tools -package unix)
$(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo)
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, -I tools -package unix)
$(OCAMLLIBDEPBYTE): tools/ocamllibdep.cmo
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call ocamlbyte, -I tools -package unix)
# The full coqdep (unused by this build, but distributed by make install)
COQDEPCMO:=clib/clib.cma lib/lib.cma tools/coqdep_lexer.cmo \
......@@ -468,24 +511,36 @@ $(COQDEP): $(call bestobj, $(COQDEPCMO))
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, $(SYSMOD))
$(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo)
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml,)
$(COQDEPBYTE): $(COQDEPCMO)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(call ocamlbyte, $(SYSMOD))
COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo
$(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO))
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, -package str,unix,threads)
$(HIDE)$(call bestocaml, -package str)
$(COQMAKEFILEBYTE): $(COQMAKEFILECMO)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(call ocamlbyte, -package str,unix,threads)
$(COQTEX): $(call bestobj, tools/coq_tex.cmo)
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, -package str)
$(COQTEXBYTE): tools/coq_tex.cmo
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(call ocamlbyte, -package str)
$(COQWC): $(call bestobj, tools/coqwc.cmo)
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, -package str)
$(COQWCBYTE): tools/coqwc.cmo
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(call ocamlbyte, -package str)
COQDOCCMO:=clib/clib.cma lib/lib.cma $(addprefix tools/coqdoc/, \
cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
......@@ -493,28 +548,45 @@ $(COQDOC): $(call bestobj, $(COQDOCCMO))
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, -package str,unix)
$(COQWORKMGR): $(call bestobj, clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo)
$(COQDOCBYTE): $(COQDOCCMO)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(call ocamlbyte, -package str,unix)
COQWORKMGRCMO:=clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo
$(COQWORKMGR): $(call bestobj, $(COQWORKMGRCMO))
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, $(SYSMOD))
$(COQWORKMGRBYTE): $(COQWORKMGRCMO)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(call ocamlbyte, $(SYSMOD))
# fake_ide : for debugging or test-suite purpose, a fake ide simulating
# a connection to coqtop -ideslave
# a connection to coqidetop
FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo \
ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo \
ide/xml_printer.cmo ide/richpp.cmo ide/xmlprotocol.cmo \
tools/fake_ide.cmo
FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo tools/fake_ide.cmo
$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP)
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, -I ide -package str,unix,threads)
$(HIDE)$(call bestocaml, -I ide -I ide/protocol -package str -package dynlink)
$(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPBYTE)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(call ocamlbyte, -I ide -package str,unix,threads)
# votour: a small vo explorer (based on the checker)
bin/votour: $(call bestobj, clib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo)
VOTOURCMO:=clib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo
bin/votour: $(call bestobj, $(VOTOURCMO))
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, -I checker)
bin/votour.byte: $(VOTOURCMO)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(call ocamlbyte, -I checker)
###########################################################################
# Csdp to micromega special targets
###########################################################################
......@@ -527,6 +599,10 @@ $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO))
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, -package num,unix)
$(CSDPCERTBYTE): $(CSDPCERTCMO)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(call ocamlbyte, -package num,unix)
###########################################################################
# tests
###########################################################################
......@@ -571,6 +647,11 @@ kernel/kernel.cma: kernel/kernel.mllib
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(VMBYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
# Specific rule for kernel.cmxa as to adjoin -cclib -lcoqrun
kernel/kernel.cmxa: kernel/kernel.mllib
$(SHOW)'OCAMLOPT -a -o $@'
$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -I kernel/byterun/ -cclib -lcoqrun -a -o $@ $(filter-out %.mllib, $^)
%.cma: %.mllib
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
......@@ -589,7 +670,7 @@ kernel/kernel.cma: kernel/kernel.mllib
$(SHOW)'OCAMLOPT -pack -o $@'
$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
COND_IDEFLAGS=$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,)
COND_IDEFLAGS=$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,)
COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,)
COND_BYTEFLAGS= \
......@@ -679,11 +760,18 @@ plugins/%.cmx: plugins/%.ml
$(SHOW)'OCAMLLEX $<'
$(HIDE)$(OCAMLLEX) -o $@ "$*.mll"
%.ml: %.ml4 $(CAMLP5DEPS)
%.ml %.mli: %.mly
$(SHOW)'OCAMLYACC $<'
$(HIDE)$(OCAMLYACC) --strict "$*.mly"
%.ml: %.ml4 $(CAMLP5DEPS) $(COQPP)
$(SHOW)'CAMLP5O $<'
$(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \
$(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@
%.ml: %.mlg $(COQPP)
$(SHOW)'COQPP $<'
$(HIDE)$(COQPP) $<
###########################################################################
# Dependencies of ML code
......
Makefile.checker
View file @ a7783b2b
......@@ -34,12 +34,26 @@ CHECKMLLIBFILE := checker/.mllibfiles
CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE))
-include $(CHECKERDEPS)
# Copied files
checker/esubst.mli: kernel/esubst.mli
cp -a $< $@
sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
checker/esubst.ml: kernel/esubst.ml
cp -a $< $@
sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
checker/names.mli: kernel/names.mli
cp -a $< $@
sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
checker/names.ml: kernel/names.ml
cp -a $< $@
sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
ifeq ($(BEST),opt)
$(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
$(STRIP) $@
$(CODESIGN) $@
$(STRIP_HIDE) $@
$(CODESIGN_HIDE) $@
else
$(CHICKEN): $(CHICKENBYTE)
cp $< $@
......@@ -57,13 +71,18 @@ checker/check.cmxa: checker/check.mllib | md5chk
$(SHOW)'OCAMLOPT -a -o $@'
$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)
$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES))
CHECKGENFILES:=$(addprefix checker/, names.mli names.ml esubst.mli esubst.ml)
CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) $(CHECKGENFILES) \
$(filter dev/checker_%, $(MLFILES) $(MLIFILES))
$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES) $(CHECKGENFILES))
$(SHOW)'OCAMLDEP checker/MLFILES checker/MLIFILES'
$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(filter checker/%, $(MLFILES) $(MLIFILES)) $(TOTARGET)
$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(CHECKMLFILES) $(TOTARGET)
$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) | $(OCAMLLIBDEP)
$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES) $(CHECKGENFILES)) | $(OCAMLLIBDEP)
$(SHOW)'OCAMLLIBDEP checker/MLLIBFILES checker/MLPACKFILES'
$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET)
$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES) $(CHECKGENFILES)) $(TOTARGET)
checker/%.cmi: checker/%.mli
$(SHOW)'OCAMLC $<'
......@@ -77,6 +96,14 @@ checker/%.cmx: checker/%.ml
$(SHOW)'OCAMLOPT $<'
$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $<
dev/checker_%.cmo: dev/checker_%.ml
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $<
dev/checker_%.cmi: dev/checker_%.mli
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $<
md5chk:
$(SHOW)'MD5SUM cic.mli'
$(HIDE)if grep -q "^MD5 $$($(OCAML) tools/md5sum.ml checker/cic.mli)$$" checker/values.ml; \
......
Makefile.ci
View file @ a7783b2b
......@@ -16,6 +16,7 @@ CI_TARGETS=ci-bedrock2 \
ci-coquelicot \
ci-corn \
ci-cpdt \
ci-cross-crypto \
ci-elpi \
ci-ext-lib \
ci-equations \
......@@ -32,6 +33,7 @@ CI_TARGETS=ci-bedrock2 \
ci-math-classes \
ci-math-comp \
ci-mtac2 \
ci-pidetop \
ci-quickchick \
ci-sf \
ci-simple-io \
......
Makefile.common
View file @ a7783b2b
......@@ -14,34 +14,48 @@
# Executables
###########################################################################
COQTOPBYTE:=bin/coqtop.byte$(EXE)
TOPBINOPT:=$(addsuffix .opt$(EXE), $(addprefix bin/, coqtop coqproofworker coqtacticworker coqqueryworker))
TOPBYTE:=$(TOPBINOPT:.opt$(EXE)=.byte$(EXE))
COQTOPEXE:=bin/coqtop$(EXE)
COQTOPBYTE:=bin/coqtop.byte$(EXE)
COQDEP:=bin/coqdep$(EXE)
COQPP:=bin/coqpp$(EXE)
COQDEPBYTE:=bin/coqdep.byte$(EXE)
COQMAKEFILE:=bin/coq_makefile$(EXE)
GALLINA:=bin/gallina$(EXE)
COQMAKEFILEBYTE:=bin/coq_makefile.byte$(EXE)
COQTEX:=bin/coq-tex$(EXE)
COQTEXBYTE:=bin/coq-tex.byte$(EXE)
COQWC:=bin/coqwc$(EXE)
COQWCBYTE:=bin/coqwc.byte$(EXE)
COQDOC:=bin/coqdoc$(EXE)
COQDOCBYTE:=bin/coqdoc.byte$(EXE)
COQC:=bin/coqc$(EXE)
COQCBYTE:=bin/coqc.byte$(EXE)
COQWORKMGR:=bin/coqworkmgr$(EXE)
COQWORKMGRBYTE:=bin/coqworkmgr.byte$(EXE)
COQMAKE_ONE_TIME_FILE:=tools/make-one-time-file.py
COQTIME_FILE_MAKER:=tools/TimeFileMaker.py
COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py
COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py
TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
$(COQWORKMGR)
TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
$(COQWORKMGR) $(COQPP)
TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\
$(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES)
COQDEPBOOT:=bin/coqdep_boot$(EXE)
COQDEPBOOTBYTE:=bin/coqdep_boot.byte$(EXE)
OCAMLLIBDEP:=bin/ocamllibdep$(EXE)
OCAMLLIBDEPBYTE:=bin/ocamllibdep.byte$(EXE)
FAKEIDE:=bin/fake_ide$(EXE)
FAKEIDEBYTE:=bin/fake_ide.byte$(EXE)
PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) $(COQDEPBOOT)
CSDPCERT:=plugins/micromega/csdpcert$(EXE)
CSDPCERTBYTE:=plugins/micromega/csdpcert.byte$(EXE)
###########################################################################
# Object and Source files
......@@ -75,13 +89,14 @@ INSTALLSH:=./install.sh
MKDIR:=install -d
CORESRCDIRS:=\
config clib lib kernel intf kernel/byterun library \
coqpp \
config clib lib kernel kernel/byterun library \
engine pretyping interp proofs parsing printing \
tactics vernac stm toplevel
PLUGINDIRS:=\
omega romega micromega quote \
setoid_ring extraction fourier \
setoid_ring extraction \
cc funind firstorder derive \
rtauto nsatz syntax btauto \
ssrmatching ltac ssr
......@@ -102,19 +117,13 @@ BYTERUN:=$(addprefix kernel/byterun/, \
# respecting this order is useful for developers that want to load or link
# the libraries directly
CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \
CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
stm/stm.cma toplevel/toplevel.cma
TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
GRAMMARCMA:=grammar/grammar.cma
# modules known by the toplevel of Coq
OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib))
###########################################################################
# plugins object files
###########################################################################
......@@ -125,20 +134,18 @@ MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
QUOTECMO:=plugins/quote/quote_plugin.cmo
RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
FOURIERCMO:=plugins/fourier/fourier_plugin.cmo
EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo
FUNINDCMO:=plugins/funind/recdef_plugin.cmo
FOCMO:=plugins/firstorder/ground_plugin.cmo
CCCMO:=plugins/cc/cc_plugin.cmo
BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo
RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo
NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo
OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
z_syntax_plugin.cmo \
SYNTAXCMO:=$(addprefix plugins/syntax/, \
r_syntax_plugin.cmo \
int31_syntax_plugin.cmo \
ascii_syntax_plugin.cmo \
string_syntax_plugin.cmo )
string_syntax_plugin.cmo \
numeral_notation_plugin.cmo)
DERIVECMO:=plugins/derive/derive_plugin.cmo
LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
......@@ -146,9 +153,9 @@ SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
$(QUOTECMO) $(RINGCMO) \
$(FOURIERCMO) $(EXTRACTIONCMO) \
$(EXTRACTIONCMO) \
$(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
$(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
$(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)
ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
......@@ -163,43 +170,8 @@ PLUGINSOPT:=$(PLUGINSCMO:.cmo=.cmxs)
LINKCMO:=$(CORECMA) $(STATICPLUGINS)
LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx)
###########################################################################
# vo files
###########################################################################
THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v"))
PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v"))
ALLVO := $(THEORIESVO) $(PLUGINSVO)
VFILES := $(ALLVO:.vo=.v)
## More specific targets
THEORIESLIGHTVO:= \
$(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO))
ALLSTDLIB := test-suite/misc/universes/all_stdlib
# convert a (stdlib) filename into a module name:
# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
ALLMODS:=$(call vo_to_mod,$(ALLVO))
# Converting a stdlib filename into native compiler filenames
# Used for install targets
vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
GLOBFILES:=$(ALLVO:.vo=.glob)
ifdef NATIVECOMPUTE
NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO))
else
NATIVEFILES :=
endif
LIBFILES:=$(ALLVO) $(NATIVEFILES) $(VFILES) $(GLOBFILES)
# For emacs:
# Local Variables:
# mode: makefile
......
Makefile.dev
View file @ a7783b2b
......@@ -17,7 +17,7 @@
.PHONY: devel printers
DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo
DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo
devel: printers
printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp5.dbg
......@@ -174,7 +174,6 @@ MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO))
QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO))
RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO))
NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO))
FOURIERVO:=$(filter plugins/fourier/%, $(PLUGINSVO))
FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO))
BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO))
RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO))
......@@ -188,7 +187,6 @@ micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
setoid_ring: $(RINGVO) $(RINGCMO)
nsatz: $(NSATZVO) $(NSATZCMO)
extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO)
fourier: $(FOURIERVO) $(FOURIERCMO)
funind: $(FUNINDCMO) $(FUNINDVO)
cc: $(CCVO) $(CCCMO)
rtauto: $(RTAUTOVO) $(RTAUTOCMO)
......@@ -196,7 +194,7 @@ btauto: $(BTAUTOVO) $(BTAUTOCMO)
ltac: $(LTACVO) $(LTACCMO)
.PHONY: omega micromega setoid_ring nsatz extraction
.PHONY: fourier funind cc rtauto btauto ltac
.PHONY: funind cc rtauto btauto ltac
# For emacs:
# Local Variables:
......
Makefile.doc
View file @ a7783b2b
......@@ -10,10 +10,7 @@
# Makefile for the Coq documentation
# To compile documentation, you need the following tools:
# Dvi: latex (latex2e), bibtex, makeindex
# Pdf: pdflatex
# Html: hevea (http://hevea.inria.fr) >= 1.05
# Read doc/README.md to learn about the dependencies
# The main entry point :
......@@ -28,23 +25,18 @@ doc-no:
######################################################################
LATEX:=latex
BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10
MAKEINDEX:=makeindex
PDFLATEX:=pdflatex
DVIPS:=dvips
HEVEA:=hevea
HEVEAOPTS:=-fix -exec xxdate.exe
HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
HTMLSTYLE:=coqremote
export TEXINPUTS:=$(HEVEALIB):
ifdef COQDOC_NOBOOT
COQTEXOPTS:=-n 72 -sl -small
else
COQTEXOPTS:=-boot -n 72 -sl -small
endif
# Sphinx-related variables
SPHINXENV:=COQBIN="$(CURDIR)/bin/"
SPHINXOPTS= -j4
SPHINXWARNERROR ?= 0
ifeq ($(SPHINXWARNERROR),1)
SPHINXOPTS += -W
endif
SPHINXBUILD= sphinx-build
SPHINXBUILDDIR= doc/sphinx/_build
......@@ -59,24 +51,23 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
.PHONY: doc doc-html doc-pdf doc-ps
.PHONY: stdlib full-stdlib sphinx
.PHONY: tutorial rectutorial
doc: refman tutorial rectutorial stdlib
doc: refman stdlib
ifndef QUICK
SPHINX_DEPS := coq
endif
# refman-html and refman-latex
refman-%: coq
refman-%: $(SPHINX_DEPS)
$(SHOW)'SPHINXBUILD doc/sphinx ($*)'
$(HIDE)COQBIN="$(abspath bin)" $(SPHINXBUILD) -b $* \
$(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \
$(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$*
refman-pdf: refman-latex
+$(MAKE) -C $(SPHINXBUILDDIR)/latex
refman: coq
refman: $(SPHINX_DEPS)
+$(MAKE) refman-html
+$(MAKE) refman-pdf
......@@ -84,19 +75,13 @@ refman: coq
sphinx: refman-html
doc-html:\
doc/tutorial/Tutorial.v.html doc/stdlib/html/index.html \
doc/RecTutorial/RecTutorial.html refman-html
doc/stdlib/html/index.html refman-html
doc-pdf:\
doc/tutorial/Tutorial.v.pdf doc/stdlib/Library.pdf \
doc/RecTutorial/RecTutorial.pdf refman-pdf
doc/stdlib/Library.pdf refman-pdf
doc-ps:\
doc/tutorial/Tutorial.v.ps \
doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.ps
tutorial: \
doc/tutorial/Tutorial.v.html doc/tutorial/Tutorial.v.ps doc/tutorial/Tutorial.v.pdf
doc/stdlib/Library.ps
stdlib: \
doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf
......@@ -104,31 +89,13 @@ stdlib: \
full-stdlib: \
doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf
rectutorial: doc/RecTutorial/RecTutorial.html \
doc/RecTutorial/RecTutorial.ps doc/RecTutorial/RecTutorial.pdf
######################################################################
### Implicit rules
######################################################################
ifdef QUICK
%.v.tex: %.tex
$(COQTEX) $(COQTEXOPTS) $<
else
%.v.tex: %.tex $(COQTEX) $(COQTOPEXE) $(ALLVO)
$(COQTEX) $(COQTEXOPTS) $<
endif
%.ps: %.dvi
(cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`)
######################################################################
# Macros for filtering outputs
######################################################################
HIDEBIBTEXINFO=| grep -v "^A level-1 auxiliary file"
SHOWMAKEINDEXERROR=egrep '^!! Input index error|^\*\* Input style error|^ --'
######################################################################
# Common
######################################################################
......@@ -138,23 +105,6 @@ SHOWMAKEINDEXERROR=egrep '^!! Input index error|^\*\* Input style error|^ --'
doc/common/version.tex: config/Makefile
printf '\\newcommand{\\coqversion}{$(VERSION)}' > doc/common/version.tex
######################################################################
# Tutorial
######################################################################
doc/tutorial/Tutorial.v.dvi: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex
(cd doc/tutorial;\
$(LATEX) -interaction=batchmode Tutorial.v;\
../tools/show_latex_messages Tutorial.v.log)
doc/tutorial/Tutorial.v.pdf: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex
(cd doc/tutorial;\
$(PDFLATEX) -interaction=batchmode Tutorial.v.tex;\
../tools/show_latex_messages Tutorial.v.log)
doc/tutorial/Tutorial.v.html: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex
(cd doc/tutorial; $(HEVEA) $(HEVEAOPTS) Tutorial.v)
######################################################################
# Standard library
######################################################################
......@@ -228,35 +178,14 @@ doc/stdlib/FullLibrary.pdf: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/s
$(PDFLATEX) -interaction=batchmode FullLibrary;\
../tools/show_latex_messages -no-overfull FullLibrary.log)
######################################################################
# Tutorial on inductive types
######################################################################
doc/RecTutorial/RecTutorial.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.tex
(cd doc/RecTutorial;\
$(LATEX) -interaction=batchmode RecTutorial;\
$(BIBTEX) -terse RecTutorial;\
$(LATEX) -interaction=batchmode RecTutorial > /dev/null;\
$(LATEX) -interaction=batchmode RecTutorial > /dev/null;\
../tools/show_latex_messages RecTutorial.log)
doc/RecTutorial/RecTutorial.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.dvi
(cd doc/RecTutorial;\
$(PDFLATEX) -interaction=batchmode RecTutorial.tex;\
../tools/show_latex_messages RecTutorial.log)
doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex
(cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial)
######################################################################
# Install all documentation files
######################################################################
.PHONY: install-doc install-doc-meta install-doc-html install-doc-printable \
install-doc-index-urls install-doc-sphinx
install-doc-sphinx install-doc-stdlib-html
install-doc: install-doc-meta install-doc-html install-doc-printable \
install-doc-index-urls install-doc-sphinx
install-doc: install-doc-meta install-doc-html install-doc-printable
install-doc-meta:
$(MKDIR) $(FULLDOCDIR)
......@@ -267,17 +196,11 @@ install-doc-html: install-doc-stdlib-html install-doc-sphinx
install-doc-stdlib-html:
$(MKDIR) $(FULLDOCDIR)/html/stdlib
$(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib
$(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html
$(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html
install-doc-printable:
$(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf
$(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf
$(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps
$(INSTALLLIB) doc/tutorial/Tutorial.v.pdf $(FULLDOCDIR)/pdf/Tutorial.pdf
$(INSTALLLIB) doc/RecTutorial/RecTutorial.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf
$(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps
$(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps
install-doc-sphinx:
$(MKDIR) $(FULLDOCDIR)/sphinx
......@@ -305,9 +228,11 @@ ODOCDOTOPTS=-dot -dot-reduce
source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
OCAMLDOC_CAML_FLAGS=-rectypes -I +threads $(MLINCLUDES)
$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
$(SHOW)'OCAMLDOC -latex -o $@'
$(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP5LIB) $(MLINCLUDES)\
$(HIDE)$(OCAMLFIND) ocamldoc -latex $(OCAMLDOC_CAML_FLAGS) \
$(DOCMLIS) -noheader -t "Coq mlis documentation" \
-intro $(OCAMLDOCDIR)/docintro -o $@.tmp
$(SHOW)'OCAMLDOC utf8 fix'
......@@ -317,31 +242,31 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
mli-doc: $(DOCMLIS:.mli=.cmi)
$(SHOW)'OCAMLDOC -html'
$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP5LIB) $(MLINCLUDES) \
$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html $(OCAMLDOC_CAML_FLAGS) \
$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
-css-style style.css
ml-dot: $(MLFILES)
$(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP5LIB) $(MLINCLUDES) \
$(OCAMLFIND) ocamldoc -dot -dot-reduce $(OCAMLDOC_CAML_FLAGS) \
$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
%_dep.png: %.dot
$(DOT) -Tpng $< -o $@
%_types.dot: %.mli
$(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
$(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -dot-types -o $@ $<
OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -o $@ \
$(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))
%.dot: | %.mllib.d
$(OCAMLDOC_MLLIBD)
ml-doc:
ml-doc: kernel/copcodes.cmi
$(SHOW)'OCAMLDOC -html'
$(HIDE)mkdir -p $(OCAMLDOCDIR)/html/implementation
$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) \
$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html $(OCAMLDOC_CAML_FLAGS) \
$(DOCMLS) -d $(OCAMLDOCDIR)/html/implementation -colorize-code \
-t "Coq mls documentation" \
-css-style ../style.css
......@@ -356,7 +281,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d
$(OCAMLDOC_MLLIBD)
%.dot: %.mli
$(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
$(OCAMLFIND) ocamldoc $(OCAMLDOC_CAML_FLAGS) $(ODOCDOTOPTS) -o $@ $<
$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
$(SHOW)'PDFLATEX $*.tex'
......
Makefile.ide
View file @ a7783b2b
......@@ -36,16 +36,18 @@ COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
# Note : for just building bin/coqide, we could only consider
# config, lib, ide and ide/utils. But the coqidetop plugin (the
# one that will be loaded by coqtop -ideslave) refers to some
# one that will be loaded by coqidetop) refers to some
# core modules of coq, for instance printing/*.
IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
IDESRCDIRS:= $(CORESRCDIRS) ide ide/protocol
COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
IDEDEPS:=clib/clib.cma lib/lib.cma
IDEDEPS:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma
IDECMA:=ide/ide.cma
IDETOPLOOPCMA=ide/coqidetop.cma
IDETOPEXE=bin/coqidetop$(EXE)
IDETOP=bin/coqidetop.opt$(EXE)
IDETOPBYTE=bin/coqidetop.byte$(EXE)
LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.mli ide/coqide_main.ml
LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.mli ide/coqide_main.ml
......@@ -88,16 +90,16 @@ endif
coqide-files: $(IDEFILES)
ide-byteloop: $(IDETOPLOOPCMA)
ide-optloop: $(IDETOPLOOPCMA:.cma=.cmxs)
ide-toploop: ide-$(BEST)loop
ide-byteloop: $(IDETOPBYTE)
ide-optloop: $(IDETOP)
ide-toploop: $(IDETOPEXE)
ifeq ($(HASCOQIDE),opt)
$(COQIDE): $(LINKIDEOPT)
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \
lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^
$(STRIP) $@
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
-linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^
$(STRIP_HIDE) $@
else
$(COQIDE): $(COQIDEBYTE)
cp $< $@
......@@ -105,8 +107,8 @@ endif
$(COQIDEBYTE): $(LINKIDE)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \
lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^
$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \
-linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp5deps here
$(SHOW)'CAMLP5O $<'
......@@ -135,6 +137,28 @@ ide/ideutils.cmx: ide/ideutils.ml
$(SHOW)'OCAMLOPT $<'
$(HIDE)$(filter-out -safe-string,$(OCAMLOPT)) $(COQIDEFLAGS) $(filter-out -safe-string,$(OPTFLAGS)) -c $<
IDETOPCMA:=ide/ide_common.cma
IDETOPCMX:=$(IDETOPCMA:.cma=.cmxa)
# Special rule for coqidetop
$(IDETOPEXE): $(IDETOP:.opt=.$(BEST))
cp $< $@
$(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
$(SYSMOD) -package camlp5.gramlib \
$(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
$(STRIP_HIDE) $@
$(CODESIGN_HIDE) $@
$(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
-I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
$(SYSMOD) -package camlp5.gramlib \
$(LINKCMO) $(IDETOPCMA) $(BYTEFLAGS) $< -o $@
####################
## Install targets
####################
......@@ -164,13 +188,11 @@ install-ide-bin:
install-ide-toploop:
ifeq ($(BEST),opt)
$(MKDIR) $(FULLCOQLIB)/toploop/
$(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
$(INSTALLBIN) $(IDETOPEXE) $(IDETOP) $(FULLBINDIR)
endif
install-ide-toploop-byte:
ifneq ($(BEST),opt)
$(MKDIR) $(FULLCOQLIB)/toploop/
$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
$(INSTALLBIN) $(IDETOPEXE) $(IDETOPBYTE) $(FULLBINDIR)
endif
install-ide-devfiles:
......@@ -206,9 +228,8 @@ $(COQIDEAPP)/Contents:
$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \
threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^
$(STRIP) $@
-linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^
$(STRIP_HIDE) $@
$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
$(MKDIR) $@/coq/
......@@ -254,7 +275,7 @@ $(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)
$(INSTALLLIB) ide/MacOS/*.icns $@
$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources
$(CODESIGN) $@
$(CODESIGN_HIDE) $@
###########################################################################
# CoqIde for Windows special targets
......