| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
| |
On bytecode platforms, Coq installs a `revision` file containing
metadata about the build. This is bad for reproducibility, so don’t
install it.
|
| |
|
|
|
|
| |
Upstream has provided a free replacement for the nonfree ssrmatching
file I removed in cf916fd97fbac51af6fa68ec2704da2a28ef9ede. Patch that
file in and resume building ssrmatching and ssreflect.
|
| |
|
|
|
|
|
|
| |
The fix-bytecode-build.patch in previous commits works fine for
building and testing, but installation still fails on bytecode
platforms – the system tries to install .cmx files that don’t exist.
Update fix-bytecode-build.patch to the latest version from Gaëtan
Gilbert, which corrects the installation targets.
|
| |
|
|
|
|
| |
Operations with .vio files fail when Coq has been compiled with ocamlc;
see https://github.com/coq/coq/issues/9141. Disable tests related
to .vio generation to prevent this from breaking the build.
|
| | |
|
| |
|
|
|
| |
This includes disabling all unit tests, which require ocamlopt and
“don’t test much yet” anyway.
|
| | |
|
| |
|
|
|
| |
Consolidate the several patches that disable tests that time out on
MIPS or use too much RAM/time on the buildds.
|
| | |
|
| |
|
|
|
| |
ocaml-best-compilers has been superseded by ocaml-nox. Simply depend on
that instead.
|
| | |
|
| | |
|
| |
|
|
| |
Upstream has switched to Markdown for their CHANGES file.
|
| | |
|
| | |
|
| |
|
|
| |
gallina(1) has been removed, so don’t try to install it.
|
| |
|
|
|
|
|
| |
As of 8.9, upstream has stopped distributing plugins that turn coqtop
into worker processes for CoqIDE and other things. There are now
separate binaries for each coqtop use case. Ensure they’re all
distributed.
|
| |
|
|
|
| |
Coq 8.9.0 introduced a test that requires oUnit. Pull it in in
debian/rules.
|
| |
|
|
|
|
|
|
| |
The nonfree file in ssrmatching I removed in
cf916fd97fbac51af6fa68ec2704da2a28ef9ede turns out to be important to
the build process, and I can’t figure out how to replicate its effects
without including the file itself. Disable ssrmatching and ssreflect
again until the license situation gets resolved.
|
| |
|
|
|
|
| |
Proof General has been designated as the official interface to Coq, and
Coq no longer ships a separate Emacs mode. Update packaging to purge
references to the Emacs mode.
|
| | |
|
| |
|
|
|
| |
Keeping patches sequentially numbered produces a messy Git history with
many renames for compaction. It’s also redundant with the series file.
|
| | |
|
| | |
|
| |
|
|
|
| |
8.9.0 deleted some files under non-DFSG-free licenses, so we no longer
need to filter out those files when importing.
|
| |
|
|
|
|
|
|
|
|
| |
Upstream has corrected most of the licensing issues with ssrmatching
in 8.9.0. That version introduced one new file with a CeCILL-B license,
but it’s an .mli file, so OCaml should be able to infer its contents.
Don’t import the offending .mli, but do import the files with corrected
license headers. Remove the patch introduced in
5d3dc22cc205021e517a81943952655c51777083 (which backported the
correctly licensed files).
|
| |
|
|
|
|
| |
$PWD doesn’t work in Makefiles – Make expands $P (to the empty string)
and passes `WD` literally to the shell. Replace `$PWD` with
`$(shell pwd)`.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
4181269ff800d58e60b886d0aaa2894444a9cd0d removed ssrmatching and
everything that needed it because upstream had shipped a couple of
files with bad license headers. Those files have now been fixed
(https://github.com/coq/coq/pull/9282), so grab them from master and
apply them in a patch. This restores ssrmatching to the Coq standard
library.
Once upstream cuts its next release, we should be able to delete the
patch and simply import the files from the upstream tarball.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Upstream deprecated it in favor of ocamlfind in
https://github.com/coq/coq/commit/598e3ae4a8eb8d9bce316e13d71ee48d9ba1a01f.
|
| |
|
|
|
| |
https://github.com/coq/coq/commit/5b506165097047aa8b6b431db9f2cbc8dbf6c3de
corrected the installation path in upstream’s build process.
|
| |
|
|
|
|
|
|
|
|
|
| |
Bytecode is no longer built by default, but it’s still essential on
Debian platforms where OCaml has no native compiler. Run `make byte`
and `make install-byte` to install bytecode.
In the future, we may want to separate bytecode binaries and libraries
into their own packages so users on platforms with native support don’t
have to spend disk space on bytecode. For now, though, continue
bundling native code and bytecode into the same package.
|
| |
|
|
|
|
| |
A number of tests (mostly for coq_makefile) assume that Coq is
installed when the test runs. This isn't true in an sbuild environment,
though, so disable those tests.
|
| |
|
|
|
|
| |
https://github.com/coq/coq/commit/bdc74cd1b945b69f81264cb6df8eb793c0c6817f
enabled debugging by default, and the flag’s since been deleted. Stop
passing it.
|
| | |
|
| |
|
|
|
|
|
| |
ssrmatching has two files licensed under CeCILL-B, which I believe is a
nonfree license. d7d80c5bea564b7cb0eadc33e9ee38c9d9de1cd8 removed those
files from the source package; this commit disables the affected plugin
in the build system.
|
| |
|
|
|
| |
Remove 0002-Remove-test-4366-too-picky-on-the-timeout.patch, since
upstream has increased the timeout.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
https://github.com/coq/coq/commit/6b4a57051a470436b50d53e7395ec44b52e2dc7e
requires rsync to collect test logs. This only really makes a
difference in Coq’s CI environment, but it’s simpler to just let it do
its thing than it is to patch the behavior out.
|
| |
|
|
|
|
|
|
|
| |
CoqIDE currently requires gtksourceview2, which has been removed from
Debian (see https://bugs.debian.org/885677). Upstream has an active
pull request to update to gtksourceview3
(https://github.com/coq/coq/pull/9279), and it looks like Debian may
ship gtksourceview2 with buster anyway, so this is likely to be a
temporary change.
|
| | |
|
| | |
|
Benjamin Barenblat