-
bac5683a
by Benjamin Barenblat
at 2019-01-17T21:33:19Z
Don’t build upstream’s CI on Salsa
-
5d3dc22c
by Benjamin Barenblat
at 2019-01-18T00:58:25Z
Restore ssrmatching and its reverse dependencies
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.
-
4b8ec4bc
by Benjamin Barenblat
at 2019-01-18T01:42:25Z
Correct environment variable settings when running tests
$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)`.
-
cf916fd9
by Benjamin Barenblat
at 2019-02-03T00:12:28Z
Prepare to import ssrmatching in 8.9.0
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).
-
3a2fac7b
by Benjamin Barenblat
at 2019-02-03T00:12:56Z
Prepare gbp to import 8.9.0
8.9.0 deleted some files under non-DFSG-free licenses, so we no longer
need to filter out those files when importing.
-
9ebf44d8
by Benjamin Barenblat
at 2019-02-03T00:29:23Z
Imported Upstream version 8.9.0
-
1ef7f1c0
by Benjamin Barenblat
at 2019-02-03T00:29:28Z
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
-
e4d4f462
by Benjamin Barenblat
at 2019-02-05T15:34:31Z
Begin packaging 8.9.0
-
4fd27468
by Benjamin Barenblat
at 2019-02-05T15:34:46Z
Update debian/copyright
-
6786da16
by Benjamin Barenblat
at 2019-02-05T15:39:11Z
Stop numbering patches
Keeping patches sequentially numbered produces a messy Git history with
many renames for compaction. It’s also redundant with the series file.
-
8300ef2c
by Benjamin Barenblat
at 2019-02-05T15:40:49Z
Refresh patches
-
956960a4
by Benjamin Barenblat
at 2019-02-05T15:43:26Z
Update packaging for Emacs mode deletion
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.
-
6e23288c
by Benjamin Barenblat
at 2019-02-05T16:24:23Z
Disable ssrmatching and ssreflect
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.
-
d0bcaaec
by Benjamin Barenblat
at 2019-02-05T16:31:43Z
Add oUnit dependency
Coq 8.9.0 introduced a test that requires oUnit. Pull it in in
debian/rules.
-
5a641c3f
by Benjamin Barenblat
at 2019-02-05T16:39:51Z
Update to new toploop packaging
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.
-
323afa78
by Benjamin Barenblat
at 2019-02-05T16:48:06Z
Don’t try to install gallina(1) (deleted by upstream)
gallina(1) has been removed, so don’t try to install it.
-
0ab72da9
by Benjamin Barenblat
at 2019-02-05T16:48:31Z
Update libcoq-ocaml{,-dev} install list
-
489e52b5
by Benjamin Barenblat
at 2019-02-05T16:57:35Z
Package new coqpp utility
-
27158c16
by Benjamin Barenblat
at 2019-02-05T16:57:57Z
s/CHANGES/CHANGES.md/
Upstream has switched to Markdown for their CHANGES file.
-
327e96d8
by Benjamin Barenblat
at 2019-02-05T17:03:43Z
Correct spelling errors
-
360aba5a
by Benjamin Barenblat
at 2019-02-05T17:04:05Z
Remove execute bit from Python libraries
-
bf8f9260
by Benjamin Barenblat
at 2019-02-05T17:30:37Z
Remove references to ocaml-best-compilers package
ocaml-best-compilers has been superseded by ocaml-nox. Simply depend on
that instead.
-
fe4de3af
by Benjamin Barenblat
at 2019-02-05T17:30:46Z
Tighten Build-Depends to match upstream’s INSTALL
-
c40a76c5
by Benjamin Barenblat
at 2019-02-05T17:30:49Z
Consolidate patches to disable tests that are too big or too slow
Consolidate the several patches that disable tests that time out on
MIPS or use too much RAM/time on the buildds.
-
4f464870
by Benjamin Barenblat
at 2019-02-05T17:30:51Z
Run tests verbosely
-
4e783ae1
by Benjamin Barenblat
at 2019-02-05T20:09:24Z
Fix build on platforms without ocamlopt
This includes disabling all unit tests, which require ocamlopt and
“don’t test much yet” anyway.
-
7cbefd56
by Benjamin Barenblat
at 2019-02-05T20:09:56Z
Disable test 4366, which is too time-sensitive for MIPS
-
4bf1d996
by Benjamin Barenblat
at 2019-02-05T21:49:08Z
Disable .vio tests, as they don’t work on bytecode architectures
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.
-
4a85cdbc
by Benjamin Barenblat
at 2019-02-06T12:24:25Z
Update fix-bytecode-build.patch to latest version
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.
-
69e02ba4
by Benjamin Barenblat
at 2019-02-06T12:37:14Z
Reenable ssrmatching and ssreflect
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.
-
8474d99e
by Benjamin Barenblat
at 2019-02-06T15:21:56Z
Don’t install the `revision` file
On bytecode platforms, Coq installs a `revision` file containing
metadata about the build. This is bad for reproducibility, so don’t
install it.
-
a7783b2b
by Benjamin Barenblat
at 2019-02-06T17:41:36Z
Release for unstable