Benjamin Barenblat pushed to branch master at Debian OCaml Maintainers / coq
Commits: 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 - - - - - 30 changed files: - − .bintray.json - .github/PULL_REQUEST_TEMPLATE.md - .gitlab-ci.yml - .merlin → .merlin.in - − .travis.yml - CHANGES → CHANGES.md - CONTRIBUTING.md - CREDITS - INSTALL - − INSTALL.doc - − INSTALL.ide - META.coq → META.coq.in - Makefile - Makefile.build - Makefile.checker - Makefile.ci - Makefile.common - Makefile.dev - Makefile.doc - Makefile.ide - Makefile.install - + Makefile.vofiles - README.md - checker/check.mllib - checker/checker.ml - checker/cic.mli - checker/closure.ml - checker/closure.mli - checker/declarations.ml - checker/declarations.mli The diff was not included because it is too large. View it on GitLab: https://salsa.debian.org/ocaml-team/coq/compare/11d2b496980a65ac1059b72275480d572634d13f...a7783b2b7b263ecf957874657b953f10b848ed7d -- View it on GitLab: https://salsa.debian.org/ocaml-team/coq/compare/11d2b496980a65ac1059b72275480d572634d13f...a7783b2b7b263ecf957874657b953f10b848ed7d You're receiving this email because of your account on salsa.debian.org.
