summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Release for unstableHEADdebian/8.9.0-1masterGravatar Benjamin Barenblat2019-02-06
|
* Don’t install the `revision` fileGravatar Benjamin Barenblat2019-02-06
| | | | | | On bytecode platforms, Coq installs a `revision` file containing metadata about the build. This is bad for reproducibility, so don’t install it.
* Reenable ssrmatching and ssreflectGravatar Benjamin Barenblat2019-02-06
| | | | | | 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.
* Update fix-bytecode-build.patch to latest versionGravatar Benjamin Barenblat2019-02-06
| | | | | | | | 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.
* Disable .vio tests, as they don’t work on bytecode architecturesGravatar Benjamin Barenblat2019-02-05
| | | | | | 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.
* Disable test 4366, which is too time-sensitive for MIPSGravatar Benjamin Barenblat2019-02-05
|
* Fix build on platforms without ocamloptGravatar Benjamin Barenblat2019-02-05
| | | | | This includes disabling all unit tests, which require ocamlopt and “don’t test much yet” anyway.
* Run tests verboselyGravatar Benjamin Barenblat2019-02-05
|
* Consolidate patches to disable tests that are too big or too slowGravatar Benjamin Barenblat2019-02-05
| | | | | Consolidate the several patches that disable tests that time out on MIPS or use too much RAM/time on the buildds.
* Tighten Build-Depends to match upstream’s INSTALLGravatar Benjamin Barenblat2019-02-05
|
* Remove references to ocaml-best-compilers packageGravatar Benjamin Barenblat2019-02-05
| | | | | ocaml-best-compilers has been superseded by ocaml-nox. Simply depend on that instead.
* Remove execute bit from Python librariesGravatar Benjamin Barenblat2019-02-05
|
* Correct spelling errorsGravatar Benjamin Barenblat2019-02-05
|
* s/CHANGES/CHANGES.md/Gravatar Benjamin Barenblat2019-02-05
| | | | Upstream has switched to Markdown for their CHANGES file.
* Package new coqpp utilityGravatar Benjamin Barenblat2019-02-05
|
* Update libcoq-ocaml{,-dev} install listGravatar Benjamin Barenblat2019-02-05
|
* Don’t try to install gallina(1) (deleted by upstream)Gravatar Benjamin Barenblat2019-02-05
| | | | gallina(1) has been removed, so don’t try to install it.
* Update to new toploop packagingGravatar Benjamin Barenblat2019-02-05
| | | | | | | 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.
* Add oUnit dependencyGravatar Benjamin Barenblat2019-02-05
| | | | | Coq 8.9.0 introduced a test that requires oUnit. Pull it in in debian/rules.
* Disable ssrmatching and ssreflectGravatar Benjamin Barenblat2019-02-05
| | | | | | | | 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.
* Update packaging for Emacs mode deletionGravatar Benjamin Barenblat2019-02-05
| | | | | | 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.
* Refresh patchesGravatar Benjamin Barenblat2019-02-05
|
* Stop numbering patchesGravatar Benjamin Barenblat2019-02-05
| | | | | Keeping patches sequentially numbered produces a messy Git history with many renames for compaction. It’s also redundant with the series file.
* Update debian/copyrightGravatar Benjamin Barenblat2019-02-05
|
* Begin packaging 8.9.0Gravatar Benjamin Barenblat2019-02-05
|
* Updated version 8.9.0 from 'upstream/8.9.0'Gravatar Benjamin Barenblat2019-02-02
|\ | | | | with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
| * Imported Upstream version 8.9.0upstream/8.9.0upstreamGravatar Benjamin Barenblat2019-02-02
| |
* | Prepare gbp to import 8.9.0Gravatar Benjamin Barenblat2019-02-02
| | | | | | | | | | 8.9.0 deleted some files under non-DFSG-free licenses, so we no longer need to filter out those files when importing.
* | Prepare to import ssrmatching in 8.9.0Gravatar Benjamin Barenblat2019-02-02
| | | | | | | | | | | | | | | | | | | | 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).
* | Correct environment variable settings when running testsGravatar Benjamin Barenblat2019-01-17
| | | | | | | | | | | | $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)`.
* | Restore ssrmatching and its reverse dependenciesGravatar Benjamin Barenblat2019-01-17
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Don’t build upstream’s CI on SalsaGravatar Benjamin Barenblat2019-01-17
| |
* | Release 8.8.2-1 for unstabledebian/8.8.2-1Gravatar Benjamin Barenblat2019-01-06
| |
* | Ignore the .pc directory when doing a buildGravatar Benjamin Barenblat2019-01-03
| |
* | Package coq_makefile’s new Python dependencyGravatar Benjamin Barenblat2019-01-03
| |
* | Correct spelling errorsGravatar Benjamin Barenblat2019-01-03
| |
* | Don't run testsuite under nocheck build profileGravatar Benjamin Barenblat2019-01-03
| |
* | Update libcoq-ocaml{,-dev} install listGravatar Benjamin Barenblat2019-01-03
| |
* | Don’t try to install coqmktopGravatar Benjamin Barenblat2019-01-03
| | | | | | | | | | Upstream deprecated it in favor of ocamlfind in https://github.com/coq/coq/commit/598e3ae4a8eb8d9bce316e13d71ee48d9ba1a01f.
* | Update coqdoc.sty installation pathGravatar Benjamin Barenblat2019-01-03
| | | | | | | | | | https://github.com/coq/coq/commit/5b506165097047aa8b6b431db9f2cbc8dbf6c3de corrected the installation path in upstream’s build process.
* | Explicitly build and install OCaml bytecode filesGravatar Benjamin Barenblat2019-01-03
| | | | | | | | | | | | | | | | | | | | | | 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.
* | Disable tests which require `-coqlib` to be setGravatar Benjamin Barenblat2019-01-03
| | | | | | | | | | | | 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.
* | debian/rules: Stop configuring with `-debug`Gravatar Benjamin Barenblat2019-01-03
| | | | | | | | | | | | https://github.com/coq/coq/commit/bdc74cd1b945b69f81264cb6df8eb793c0c6817f enabled debugging by default, and the flag’s since been deleted. Stop passing it.
* | debian/rules: Bump Coq versionGravatar Benjamin Barenblat2019-01-03
| |
* | Disable ssrmatchingGravatar Benjamin Barenblat2019-01-03
| | | | | | | | | | | | | | 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.
* | Refresh patchesGravatar Benjamin Barenblat2019-01-03
| | | | | | | | | | Remove 0002-Remove-test-4366-too-picky-on-the-timeout.patch, since upstream has increased the timeout.
* | Install upstream’s CHANGESGravatar Benjamin Barenblat2019-01-03
| |
* | debian/copyright: Audit and updateGravatar Benjamin Barenblat2019-01-03
| |
* | debian/control: Update build dependenciesGravatar Benjamin Barenblat2019-01-03
| | | | | | | | | | | | | | 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.
* | Stop distributing CoqIDEGravatar Benjamin Barenblat2019-01-03
| | | | | | | | | | | | | | | | | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-30 23:43:53 +0000