| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
Coq has introduced many new files in the last couple of years,
including several that are not DFSG-free. Rebuild and document the list
of files to be excluded from git-buildpackage imports.
Additionally, delete the purify_tarball script, as it’s been replaced
with the import filter.
|
| |
|
|
|
|
|
|
| |
The Coq developers now distribute Coq through GitHub rather than via a
direct download from INRIA. Update debian/watch to point to GitHub.
Tweak the version regex slightly to account for Coq using capital V in
their version numbers (e.g., V8.7.2). Also tweak the regex to ignore
any release with a + in it; those releases are preproduction releases.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
Benjamin Barenblat
Stephane Glondu
Enrico Tassi