Nightly builds roadmap - Githubissues

Zimmi48 commented 6 years ago

Providing nightly Coq builds would simply mean having a webpage where users can download a binary package corresponding to the latest version of Coq master branch. This should include at least the packages we provide now for released versions (MacOS, Windows 32 bits and Windows 64 bits) but it would be cool to provide more (e.g. a Debian / Ubuntu .deb binary package, a Nix package with a binary cache, etc).

Nightly builds are useful to ensure that all our users have the possibility of testing development (alpha) versions, including those who are on platforms where compiling Coq from sources is harder. In particular, developers of Coq packages we test in CI must be able to run their packages with the latest version of Coq master. Additionally, providing a pre-compiled Linux package (.deb or Nix) would help gain build time for people testing their package on CI with the development version of Coq.

We are already quite close to providing nightly builds. Here are the steps I see:

[x] Build MacOS and Windows packages on CI.
[x] (optional) Build Linux binary packages on CI (done with Nix).
[x] Give a precise version number to these packages. See coq/coq#483. What is the current status of this PR? @ejgallego do you intend to take care of finishing it and do you think that Dune is going to help here?
[x] Choose where to host these packages. Because Travis doesn't provide native build artifact support, the MacOS package currently uses bintray. With a proper version number, it would make sense to use this platform for nightly builds and we could upload Windows package over there as well.

ejgallego commented 6 years ago

What is the current status of this PR? @ejgallego do you intend to take care of finishing it and do you think that Dune is going to help here?

The PR was in need of some make hackery, so yes and yes.

JasonGross commented 6 years ago

Note that I have ~nightly builds at https://launchpad.net/~jgross-h/+archive/ubuntu/coq-master-daily, https://launchpad.net/~jgross-h/+archive/ubuntu/coq-8.8-daily, etc, and packages for the various released versions at https://launchpad.net/~jgross-h/+archive/ubuntu/many-coq-versions . I do not endorse using the scripts that I'm using to do this; they are cargo-culted from the released debian packages and have many artifacts because of that. I made them basically just so that I could test whatever versions of Coq I wanted on travis without needing to wait for them to build.

Zimmi48 commented 6 years ago

@maximedenes @ejgallego @SkySkimmer once the MacOS and Windows packages are built on GitLab CI, will there be a natural place to store them and distribute them to users?

Zimmi48 commented 6 years ago

Note that ideally we want a way for them to find the packages corresponding to a given (recent) commit hash (even if coq/coq#483 hasn't landed yet).

SkySkimmer commented 6 years ago

They will appear as artifacts. You can get current artifacts for the branch, eg https://gitlab.com/SkySkimmer/coq/-/jobs/artifacts/master/download?job=build (https://docs.gitlab.com/ee/user/project/pipelines/job_artifacts.html#downloading-the-latest-artifacts) There doesn't seem to be a way to get artifacts for a given commit without first somehow choosing a pipeline for that commit.

Currently artifacts are set to be deleted after a week (except for test suite failure logs). If we start directing people to them we should actually consider if and when we want to expire them rather than me randomly picking something. We can always hit "keep" for specific ones (eg for tags).

Zimmi48 commented 6 years ago

In coq/www#69, I'm using the canonical address for GitLab CI artifacts to direct people to a development version of the reference manual.

andres-erbsen commented 6 years ago

I would love to see officially supported binary packages for Linux -- I also have my own hacky homegrown solution for producing them which I would like to replace. For me the use cases are both CI and interactive, and I think a reasonable sketch of the requirements is:

1) usable without root access 2) fast to unpack 3) either do not depend on ocaml (no native_compute), include ocaml, or provide supported instructions for downloading and using a separate binary package 4) support Arch Linux, Debian stable, latest Ubuntu release, and latest Ubuntu LTS

Additional nice-to-haves:

5) "portable": support these distributions using a single package that works just because it does not depend on the system details 6) path-independent: the package works regardless of where it is unpacked (I don't know whether my current setup provides this...) 7) include ocaml, or provide supported instructions for downloading and using a separate binary package 8) feature parity with the windows packages (plugins, etc). In particular, I currently use Ltac1 by default, and I think having confidence in having Ltac2 available as easily as coq would flip that. coq/coq#8557 9) small downloads, as long as it does not increase unpacking time

gares commented 6 years ago

Additionally, providing a pre-compiled Linux package (.deb or Nix) would help gain build time for people testing their package on CI with the development version of Coq.

I think the build time for Coq alone is negligible (if you have an opam root ready). So I don't see the point of doing this unless we also put in the package a bunch of user contributions, as we do in the windows installer.

Zimmi48 commented 6 years ago

Note that we are now routinely building a Nix binary that is usable on any Linux / macOS with Nix installed. I should write documentation on how to install it.

@andres-erbsen Your point about addons is interesting. We included these addons in the Windows package because it was much more complicated to get them compared to Linux / macOS, but now the situation is reversed and it is (comparatively) harder to get them on Linux / macOS than on Windows.

@gares I disagree: a build time of 10 minutes is certainly not negligible for a normal CI (disclaimer: Coq is not a good example of a normal CI). E.g. each of the builds of the lemma-overloading package take 3 to 5 minutes (https://travis-ci.com/coq-community/lemma-overloading/builds/85870165). It would certainly be a burden to push this up to 15 minutes.

ejgallego commented 6 years ago

Nix seems indeed like a good candidate for that, Docker is maybe too heavy and not so user-friendly.

gares commented 6 years ago

Nightly builds are useful to ensure that all our users

@Zimmi48 I thought you were doing this for human users. CI is another matter, and I agree 10 minutes are a lot there

Zimmi48 commented 6 years ago

@gares Regarding the part you just quoted I was mostly thinking of Windows users when I wrote this.

So yes: one goal is to support easy access to the development version for all humans, including humans on Windows (OPAM or Nix are already enough for Linux and macOS users, although it gets more complex if you want to also test the latest CoqIDE on macOS), and another goal is to support CI (see also coq/coq#7753). Finally, one third goal that wasn't initially included in this issue is to provide pre-compiled Coq packages as well. This is something I'm working on as part of my experiments in coq-community.

Zimmi48 commented 5 years ago

In coq/coq#8941, it was said that:

Debian packages for Coq should be dropped from the official channels
We could provide our own .deb packages (like it used to be the case) and @gares has experience with this so he could create the initial version, but it would be a pain to maintain.
A probably better idea to solve the problem of install on Linux for non-technical users (problem that was mentioned by @amahboubi at the last WG) would be to provide a binary package, for instance as a snap. We should evaluate the cost of maintaining this. It could probably include a full opam root, etc. I have also wondered about the feasibility of making a snap out of the Nix package but I don't have time to look into this.

andres-erbsen commented 5 years ago

I am now trying out http://rgrinberg.com/posts/static-binaries-tutorial/ to make a pre-compiled tarball...

JasonGross commented 5 years ago

We could provide our own .deb packages (like it used to be the case) and @gares has experience with this so he could create the initial version, but it would be a pain to maintain.

I have also been maintaining nightly .deb packages, as well as all of the released version back to ~8.3.X, built on launchpad. The packaging scripts are a mess, but they work and tend to not be hard to maintain; the biggest headache by at least two orders of magnitude is dealing with dependency version bumps. (I believe @bbarenblat is also looking into updating ubuntu/debian packages at some point in the near future.)

andres-erbsen commented 5 years ago

Initial results for static linking against musl seem promising. In particular, coq master coqtop built on the docker image ocaml/opam:alpine_ocaml-4.06.0_flambda starts on current Arch Linux and Ubuntu 16.04.5. The patch I used:

diff --git a/configure.ml b/configure.ml
index 39c65683f..499ef81f8 100644
--- a/configure.ml
+++ b/configure.ml
@@ -486,7 +486,7 @@ let coq_bin_annot_flag = if !prefs.bin_annot then "-bin-annot" else ""
 let coq_safe_string = "-safe-string"
 let coq_strict_sequence = "-strict-sequence"

-let cflags = "-Wall -Wno-unused -g -O2"
+let cflags = "-static -Wall -Wno-unused -g -O2"

 (** * Architecture *)

@@ -654,7 +654,7 @@ let coq_warn_error =

 (* Flags used to compile Coq and plugins (via coq_makefile) *)
 let caml_flags =
-  Printf.sprintf "-thread -rectypes %s %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string coq_strict_sequence
+  Printf.sprintf "-ccopt -static -thread -rectypes %s %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string coq_strict_sequence

 (* Flags used to compile Coq but _not_ plugins (via coq_makefile) *)
 let coq_caml_flags =

andres-erbsen commented 5 years ago

This looks rather promising; statically linking coq (with the above patch) against musl seems to work.

However, it would be nice to also statically link and bundle the matched version of ocaml for compilation of plugins (afaik that is blocking for @JasonGross to move away from .dev packages). I tried, but couldn't get it to work in an hour. https://gist.github.com/andres-erbsen/2139718c00b268e9c5bf658cbcd62d75 fails to link Mltop into coqtop (https://gist.github.com/andres-erbsen/6b28f732e01cebe2dad97fef7cb5deaa). I still don't understand ocaml linking enough to make progress on this.

ejgallego commented 5 years ago

I'd recommend you use the Dune-based build for this.

However, it would be nice to also statically link and bundle the matched version of ocaml for compilation of plugins

What do you mean? Distributing a full OCaml compiler? Then again I'd suggest you use the dunerized version of OCaml [it has landed on trunk, dunno about 4.07] à la OCaml platform, however whether that will work with static linking / musl, I remain skeptical.

ejgallego commented 5 years ago

Error: No implementations provided for the following modules: Dynlink referenced from lib/lib.cmxa(System),

Umm, you basically told the OCaml compiler that the system has no dynamic linking, thus no point in compiling plugins; you could provide a stub for Dynlink, however no point on compiling plugins as you won't be able to load them.

ejgallego commented 5 years ago

Anyways I am not sure why you want to statically link coq; I don't see a point as it only depends on libc and that should be ABI compatible provided you have a bit of care with the build env.

andres-erbsen commented 5 years ago

Statically linking coq has so far been the only way I have managed to get the same coq binary to run on the computers I used to test here. Otherwise the errors have been exactly due to failing to find a compatible libc. I see static linking as a necessary prerequisite for portable packages.

As coq plugins can only be built with a matching ocaml version, a binary package of coq is much more useful it comes with instructions for how to get a matching ocaml. Perhaps I should have searched the internet for a statically linked ocaml instead of trying to make one. Is there a recommended one?

As for dune, yes, I agree that I should switch, just haven't learned the ways yet.

andres-erbsen commented 5 years ago

Okay, I can't figure out how to build ocaml using dune:

browse@ashryn ~/ocaml (git)-[trunk] % git diff  
diff --git a/dune b/dune
index 57843d9ef..28de06827 100644
--- a/dune
+++ b/dune
@@ -138,7 +138,7 @@
 (executable
  (name main)
  (modes byte)- (flags (:standard -principal -nostdlib))
+ (flags (:standard -ccopt -static -principal -nostdlib))
  (libraries ocamlbytecomp ocamlcommon runtime stdlib)
  (modules main))

@@ -152,7 +152,7 @@
 (executable
  (name optmain)
  (modes byte)
- (flags (:standard -principal -nostdlib))
+ (flags (:standard -ccopt -static -principal -nostdlib))
  (libraries ocamloptcomp ocamlcommon runtime stdlib)
  (modules optmain))

browse@ashryn ~/ocaml (git)-[trunk] % dune build
browse@ashryn ~/ocaml (git)-[trunk] % # nothing happened

ejgallego commented 5 years ago

Okay, I can't figure out how to build ocaml using dune:

Sorry I didn't explain properly you are walking into extremely experimental stuff. I've just checked and the amount of Dune support in OCaml won't suffice to get a working OCaml+Coq yet. Thus your bet is opam 2.0 local switches _opam.

Does dune build @world work?

ejgallego commented 5 years ago

You need to run configure first BTW.

ejgallego commented 5 years ago

On the good side when things are ready the process should be very straighforward.

ejgallego commented 5 years ago

Note that by the way I was suggesting to use Dune for building Coq; this part is almost ready and would be interesting to setup.

JasonGross commented 5 years ago

Does dune build @world work?

For me, dune build @world gives many instances of Error: Unbound module Pervasives.

ejgallego commented 5 years ago

Are you in a clean tree? It does work for me (TM):

$ # ocaml ref cbefaee43
$ ./configure
$ dune build @world
$ _build/default/ocamlc.byte --version
4.08.0+dev0-2018-04-09

anyways I am sorry I pointed you folks to OCaml + Dune, this is certainly not ready yet unless you are interested in Dune itself and want to do low level hacking.

Zimmi48 commented 5 years ago

The snap approach is not to statically link everything together but rather to pack all the dependencies together as in a sort of chroot IIUC.

gares commented 5 years ago

I've a POC for snap, see coq/platform#30 .

MSoegtropIMC commented 5 years ago

I wonder how easy it is to maintain a binary distribution of CoqIDE. On Windows, it links to about 30 DLLs, mostly GTK, cairo, pango, internationalization... In my personal experience with using binary distributions e.g. for proprietary CAD software, this looks non-trivial and rather maintenance intensive. Is the idea to also supply everything which is not absolutely core OS as on Windows?

What about RedHat and Suse Linux, which are (as far as I can tell) in industrial engineering environments more common than Debian / Ubuntu / Fedora / Mint / Arch.

gares commented 5 years ago

The main difference wrt building a binary bundle on windows is that, on Linux, you can use the distribution itself in order to gather most of the binaries. I did not dig too deep, but my impression is that when I did build the snap package it downloaded an ubuntu image, run my script on top of it, and then made an image of the resulting files. Then the image is executed in a container, it's a chroot roughly.

Long story short, the maintenance cost seem to be mostly on the base image (ubuntu here).

I don't like this approach much (you duplicate code, bugs, and make security updates impossible to centralize) but I also see the advantage of not having to build 30 different packages in order to distribute a software for Linux. You may need to rebuild your package on an updated base image if the copy of SSL you did originally bundle turns out to be broken, but that's all I guess.

MSoegtropIMC commented 5 years ago

@gares: thanks for the explanation! Did you test this on Redhat / Suse as well? It sounds like something which is more likely to work on Debian based distros. But I anyway don't think that this is much of an option for industrial folks for security reasons. What would make more sense in my world is to support say 3 or 4 specific versions of major distributions in a more direct way. This should help a good fraction of the users and would also provide enough template material for others.

gares commented 5 years ago

Did you test this on Redhat / Suse as well?

RHL provides a competitor to snap, called flatpak. Fedora and opensuse support snap. My impression is that RHL lost this one to Canonical, in particular the flatpak store seem to contain mainly free software, while the snap one also commercial software.

Let me just recall we are talking about nightly builds here, so I don't think any security concern really applies (you don't use a nightly build in production). I think at snaps as a sort of "tarball with all the binaries" with the advantage that they are easy to build (the tool does the transitive closure for you). Convenient, but not very professional. It may work for some users.

ejgallego commented 5 years ago

I am tempted to close this @Zimmi48 ; IMO, we are good here [modulo of course providing more formats suck as snap]

The versioning issues are tricky and IMO should be addressed in their own PR.

Zimmi48 commented 5 years ago

Sorry but we are not good. There is no way to discover the Windows package for master and the macOS package isn't even built anymore. Though, I agree that snap support could be followed in its own issue and the versioning question is tricky.

MSoegtropIMC commented 5 years ago

There is no way to discover the Windows package for master

@Zimmi48 : can you explain a bit what you mean by this?

Zimmi48 commented 5 years ago

I mean that after we are satisfied with our solution for building Windows packages (e.g. probably after moving this to Azure pipelines), we need to document on the website how users can find the packages for Coq master. We also need to solve the issue regarding the open source archive (probably by ensuring that this open source archive cannot change from one build to the next to avoid recreating it each time).

MSoegtropIMC commented 5 years ago

I see.

probably by ensuring that this open source archive cannot change from one build to the next to avoid recreating it each time

This would work for the cygwin packages but possibly not for other packages. Cygwin can be kept fixed during each release period by various means, but obviously we can't keep addons fixed. LGPL addons would be fine, but it is a lot of effort to keep track of all licenses.

Zimmi48 commented 5 years ago

I wouldn't worry about the addons. All of them have public git repositories, and are developed by people that we know. If someone were to request the source code of these addons to us, we would know where to tell them to look for it, which is not necessarily the case with the cygwin bundle.

MSoegtropIMC commented 5 years ago

For industrial users, it is also an important question if a piece of software doesn't just follow the spirit of the license but also fulfills the legal requirement. Most of the stuff has a permissive open source license like LGPL but there are a few exceptions, notably the CompCert frontend is GPL. So if the installer contains compiled versions of the CompCert frontend (which it does) we must provide the source code directly. The GPL does not allow delegation of the source code access. This is a bit old fashioned and comes from the pre-github times, but it is the way it is. Of cause it is not terribly likely that one of the addon providers sues the Coq team on this, but industrial customers tend to review the possibility of something like this happening and for industrial customers it is an important quality criterion that this is handled properly.

But it might make sense to have an archive of zips which doesn't duplicate zips and just deliver a list of files to download from this archive. The same might make sense for the cygwin part. This would very subsantially cut down the effort for creating the open source archive.

Zimmi48 commented 5 years ago

I was not talking about respecting the spirit of the license only. I know pretty well the reasons for this open source archive.

we must provide the source code directly

That's wrong. We must provide the license directly, which informs the user that they can request the source code, and we must provide the source code upon request. The only inconvenience of not providing the source code directly is that theoretically the GPL 2.0 license would allow a user to request a hard-copy of the source code. But we could still charge them for the burning and mailing fees, so that's not too bad.

The GPL does not allow delegation of the source code access.

Right, but what I mean is that if someone requests the source code, we know where to find it with addons, so that we can then send it to the user, whereas it is less clear with Cygwin modules.

Zimmi48 commented 5 years ago

But it might make sense to have an archive of zips which doesn't duplicate zips and just deliver a list of files to download from this archive. The same might make sense for the cygwin part. This would very subsantially cut down the effort for creating the open source archive.

I didn't understand this part.

MSoegtropIMC commented 5 years ago

we must provide the source code directly

I didn't mean that we have to provide it for immediate download. I meant that we have to provide it. If we don't provide it for download in an obvious way, the license must include an address whom to contact and this address must be monitored for a certain period after the release. Typically it is considered the most feasible method to provide it for immediate download.

I didn't understand this part.

I meant that if we provide sources for daily builds, this would be highly redundant (in terms of upload bandwidth). Since the sources of plugins (and cygwin stuff) doesn't change that regularly, it would be an option to upload each source package separately, and only if it isn't there as yet, and for each version provide a list of which files are part of the source archive (e.g. in form of a wget shell script).

Zimmi48 commented 5 years ago

OK.

In any case, I think it would be better if we could avoid storing large quantities of source code that is already stored elsewhere. We could try piggy-backing on Software Heritage https://www.softwareheritage.org/archive/ (which has an API), to ensure that all the sources of dependencies and add-ons that we build into our packages are stored somewhere permanently. Then, we could provide a simple shell script (included within the installer) that downloads the source of all dependencies and add-ons on the user's machine whenever it is run.

MSoegtropIMC commented 5 years ago

We could try piggy-backing on Software Heritage

This looks good, yes. One could also ask the FSF for an official opinion if just providing github and gitlab links with exact hashes would be fine.

Btw.: providing git references to the INRIA gitlab should be fine, since INRIA is the provider of the binaries. But this would but some requirements on the lifetime of the INRIA GIT after each release, which should be discussed upfront with the gitlab responsible at INRIA.

I guess it would be best to have a bit of a shared strategy and in the end provide a script which reconstructs the source code from wherever it is. The working of this script should also be tested in CI. Cygwin repos btw. usually only keep the current and 2 previous versions, so for cygwin it is more critical to keep the sources.

ejgallego commented 3 years ago

All we need here is IMHO a bit more documentation.

Zimmi48 commented 3 years ago

My impression is also that the work on the Coq platform has solved most of what was discussed (in particular, we do provide a Snap binary package now).

Nightly built binaries aren't actually that useful to end-users, but they are now produced by the Coq platform CI: https://github.com/coq/platform/actions (see the artifact section in the latest "Coq Platform CI" and "Snap package" jobs). Users can also rely on opam to build the development version of Coq, even on Windows thanks to the platform's scripts.

Finally, there is the option of relying on Nix to get a pre-compiled Coq for any released version or the latest development version. We are working on improving the situation with respect to this with @CohenCyril, and we should update the corresponding documentation. See https://github.com/coq-community/templates/issues/69.

MSoegtropIMC commented 3 years ago

Please note that currently the Coq platform CI is for the latest release and and not the dev. I plan to change this soon such that the nightly build is done for both, release and dev versions (by merging the branches together again).

Zimmi48 commented 3 years ago

OK, thanks for clarifying!

coq / platform

Nightly builds roadmap #108