Stream: Coq users

Topic: My first Coq opam package

Assia Mahboubi (May 27 2020 at 15:22):

Hi. I am trying to create an opam package for the first time. I am following this documentation page. The current version of my package definition file is here. I think that so far I have followed the documentation to the letter. And now I would like to try my stuff, as suggested. But I get an error that I do not know how to deal with (see below, sorry for the line in French). It looks like a stupid mistake: can someone help?

$ opam install -v coq-mathcomp-apery
The following actions will be performed:
  ∗ install coq-mathcomp-apery 1.0.0

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+ /home/assia/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j7" (CWD=/home/assia/.opam/current-coq/.opam-switch/build/coq-mathcomp-apery.1.0.0)
- make: *** Pas de cible spécifiée et aucun makefile n'a été trouvé. Arrêt.
[ERROR] The compilation of coq-mathcomp-apery failed at
        "/home/assia/.opam/opam-init/hooks/sandbox.sh build make -j7".

#=== ERROR while compiling coq-mathcomp-apery.1.0.0 ===========================#
# context     2.0.4 | linux/x86_64 | ocaml-base-compiler.4.09.0 | file:///home/assia/Repos/opam-coq-archive/released
# path        ~/.opam/current-coq/.opam-switch/build/coq-mathcomp-apery.1.0.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j7
# exit-code   2
# env-file    ~/.opam/log/coq-mathcomp-apery-21638-9b8556.env
# output-file ~/.opam/log/coq-mathcomp-apery-21638-9b8556.out
### output ###
# make: *** Pas de cible spécifiée et aucun makefile n'a été trouvé. Arrêt.



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coq-mathcomp-apery 1.0.0
└─
╶─ No changes have been performed
'opam install -v coq-mathcomp-apery' failed.

Théo Zimmermann (May 27 2020 at 15:30):

I can't seem to see the issue. Could this be a bug of your Makefile not behaving as you would have expected?

Assia Mahboubi (May 27 2020 at 15:31):

A make local to the repo directory, and in an opam switch with all the necessary dependencies installed works like a charm and compiles everything.

Assia Mahboubi (May 27 2020 at 15:33):

Is there anything else I should expect from the Makefile?

Cyril Cohen (May 27 2020 at 15:45):

Can you provide the contents of ~/.opam/log/coq-mathcomp-apery-21638-9b8556.env and ~/.opam/log/coq-mathcomp-apery-21638-9b8556.out?

Gaëtan Gilbert (May 27 2020 at 15:45):

For a non .dev version you need the url

Cyril Cohen (May 27 2020 at 15:46):

oh I understand, you are indeed missing the section

url {
  src: "https://github.com/$YOU/foo/archive/1.0.0.tar.gz"
  checksum: "sha256=133f2c6de1b9b35c0b26ab3e21fa86a351fffb415d20cae714b015f95fbc3725"
}

Cyril Cohen (May 27 2020 at 15:48):

In fact, there is no way to know, since you point us to https://github.com/math-comp/apery/blob/master/coq-mathcomp-apery.opam which is not supposed to have a url section, while you are visibly at the "Test your new package" step of the https://coq.inria.fr/opam-packaging.html manual

Cyril Cohen (May 27 2020 at 15:48):

can you provide the content of released/packages/coq-mathcomp-apery/coq-mathcomp-apery-1.0.0/opam in your local clone of opam-coq-archive?

Enrico Tassi (May 27 2020 at 15:51):

The url stanza is new in opam2, maybe the Coq doc was not updated?
I did the same mistake before, if you forget that stanza then OPAM downloads no tarball but still runs your commands, hence make complaining there is no Makefile...

Enrico Tassi (May 27 2020 at 15:51):

Indeed the doc lacks the url stanza in the example :-/

Théo Zimmermann (May 27 2020 at 15:52):

The doc was updated to opam 2 but this was probably forgotten.

Enrico Tassi (May 27 2020 at 15:53):

I'm wrong, the doc has it in the example

Cyril Cohen (May 27 2020 at 15:53):

Shouldn't there be a fake template opam package that is checked by the CI and refered to in the manual, so that at least templates do not fall out of sync?

Théo Zimmermann (May 27 2020 at 15:56):

Note that we do have a template opam package here: https://github.com/coq-community/templates. However, this is the version to be committed in the repo, so it doesn't have the url part.

Enrico Tassi (May 27 2020 at 15:56):

Yup, @Assia Mahboubi I believe you missed on step, the one doing curl -L https://github.com/$YOU/foo/archive/1.0.0.tar.gz | sha256sum...

Assia Mahboubi (May 27 2020 at 17:41):

Many thanks to you all for all the messages. I realize that I have indeed not followed the doc "to the letter". Actually my initial goal was to set up CI for this code. And thus to write an opam file for this purpose. I did not realize that the opam file which is in the repo of the code can be different from the one which is in the opam-coq-archive repository.... Hence I started with this template and this page says "Later on, you may want to publish your package in opam. You can just take this file content and create a pull-request on the Coq repository. " So indeed, I did not realize that this is not completely accurate.

Assia Mahboubi (May 27 2020 at 17:44):

In fact, I also had a look at other (local) opam files like this one, which does not feature an url field either, so it kept me confused.

Assia Mahboubi (May 27 2020 at 17:45):

I will try what you suggest (when time allows) and give feedback but I have a silly question: if this field is required why linting doesn't detect that it is absent?

Cyril Cohen (May 27 2020 at 17:47):

@Assia Mahboubi the url field is not always required, in local and dev packages for example, I guess this is why the linter succeeds (it does not know in which context you are...)

Cyril Cohen (May 27 2020 at 17:49):

All local pacakges you might have taken as an example will exclude the url, (since the opam is expected to take the directory which contains the opam file as a source). Publishing opam packages nowadays consists in adding the url.
BTW I automatized this a while ago in mathcomp https://github.com/math-comp/math-comp/blob/master/etc/utils/packager but I believe coq should provide a tool to do that for any package...

Assia Mahboubi (May 27 2020 at 17:58):

@Cyril Cohen it could emit a warning: if the field can be required, this could be useful.

Assia Mahboubi (May 27 2020 at 17:59):

Thanks for the pointer to the packager, but what is this script supposed to do exactly?

Assia Mahboubi (May 27 2020 at 18:00):

As a conclusion, what is the appropriate workflow for creating opam config file(s) for both CI and packaging?

Cyril Cohen (May 27 2020 at 18:00):

Playing around with the options of opam lint, maybe the documentation should suggest adding --check-upstream which will try to download the archive and check its checksum, and fail if the url field is not provided or if the url is invalid (or bad checksumed)

Karl Palmskog (May 27 2020 at 18:00):

@Cyril Cohen we (in coq-community) believe using/adapting dune-release could be a better option for the long term, at least if the project uses dune for building (https://github.com/ocamllabs/dune-release). That's not to say packager doesn't solve the problem, but hooking in to the ecosystem might become more valuable over time.

Cyril Cohen (May 27 2020 at 18:02):

Assia Mahboubi said:

Thanks for the point to the packager, but what is this script supposed to do exactly?

it is supposed to take all the ".opam" declarations at the root of math-comp + versions and other arguments described in the header (and while running the command with no arguments) and make publishable opam packages.

Cyril Cohen (May 27 2020 at 18:03):

Karl Palmskog said:

Cyril Cohen we (in coq-community) believe using/adapting dune-release could be a better option for the long term, at least if the project uses dune for building (https://github.com/ocamllabs/dune-release). That's not to say packager doesn't solve the problem, but hooking in to the ecosystem might become more valuable over time.

I did not switch to dune yet for my developments and I am a bit reluctant to do so until coq endorses it officially.

Assia Mahboubi (May 27 2020 at 18:51):

make publishable opam packages.

What does this mean exactly @Cyril Cohen ? That it generates the package description file? That it creates the corresponding data in an existing fork of opam-coq-archive? something else?

Assia Mahboubi (May 27 2020 at 18:57):

More over, if I understand correctly your answer is for publishing packages. But my question was more about the workflow for simultaneously generating the opam description to be put in the repository, for CI purposes, and the opam description to be submitted to the opam-coq-archive. I just discovered that they are different, when @Guillaume Claret 's tutorial for CI seemed to suggest that they could be the same.

Cyril Cohen (May 27 2020 at 19:09):

It is for generating the publishable packages i.e. opam files augmented with the url field, in a directory tree of the right shape, ready for doing a mv in a clone of opam-coq-archive that you still have to do yourself. (This could be further automatized of course)

Cyril Cohen (May 27 2020 at 19:10):

The local opam file already serves the CI purposes

Karl Palmskog (May 27 2020 at 19:11):

local opam files are also very useful for pinning from the local filesystem outside of CI

Assia Mahboubi (May 27 2020 at 19:14):

Sorry for the silly questions, but I still do not get it: why should local opam files be different from opam files to be add to opam-coq-archive?

Assia Mahboubi (May 27 2020 at 19:19):

@Cyril Cohen I am trying to rephrase: the packager script takes a local opam file (suitable for CI purposes) + additional information passed as arguments, and generate a new opam description file (sutable for packaging purposes), and it works if called at the right place "in a directory tree of the right shape" (i.e. this is hard-coded in the script). Correct?

Christian Doczkal (May 27 2020 at 19:31):

Assia Mahboubi said:

Sorry for the silly questions, but I still do not get it: why should local opam files be different from opam files to be add to opam-coq-archive?

Here are two reasons: the local opam file in the repository should build and install the files it is surrounded by. So it doesn't need a URL field and it's version is usually "dev". The opam files in opam-coq-archive should (mostly) install released versions. And since the archive only contains the opam file but not the development, it also needs the URL (usually to the .tar archive of a release) in order to fetch the files to be installed.

Cyril Cohen (May 27 2020 at 19:35):

Assia Mahboubi said:

Cyril Cohen I am trying to rephrase: the packager script takes a local opam file (suitable for CI purposes) + additional information passed as arguments, and generate a new opam description file (sutable for packaging purposes), and it works if called at the right place "in a directory tree of the right shape" (i.e. this is hard-coded in the script). Correct?

Correct until "a new opam description file...", instead it generates 6 new opam files (suitable for packaging purposes, i.e. with url fields added compared to the local opam files, with the following paths released/coq-mathcomp-${package}/coq-mathcomp-${package}.${version}/opam so that already fits the directory shape imposed by the opam-coq-archive repo.

Cyril Cohen (May 27 2020 at 19:40):

Cyril Cohen said:

Playing around with the options of opam lint, maybe the documentation should suggest adding --check-upstream which will try to download the archive and check its checksum, and fail if the url field is not provided or if the url is invalid (or bad checksumed)

I opened a PR coq/www#147 to get an error message when one does not put the url field.

Théo Zimmermann (May 27 2020 at 19:56):

If you are looking for a way of setting up opam for CI, the easiest way today would be to use the templates at https://github.com/coq-community/templates

Théo Zimmermann (May 27 2020 at 19:56):

We already support generating the opam file, a .travis.yml file or a GitHub Action workflow, and there's an open PR to also have a CircleCI template.

Christian Doczkal (May 27 2020 at 20:01):

Last time I checked, the templates did not yet support basing the CI jobs on mathcomp images. If one is using more than just the ssreflect component, then this may not be the best solution (yet).

Karl Palmskog (May 27 2020 at 20:17):

if support for mathcomp CI images is what's holding back template adoption for MathComp projects, I'm sure we could add some parametrization for this, feel free to open an issue

Assia Mahboubi (May 27 2020 at 20:43):

Thanks for the suggestions @Théo Zimmermann @Karl Palmskog ! I will have a look at the templates from coq-community (which I was not aware of, shame on me) and will try to provide feedback.

Karl Palmskog (May 27 2020 at 20:45):

@Assia Mahboubi it may be helpful to look at some MathComp-related projects that fully use the templates (specifically examples of meta.yml), e.g., https://github.com/coq-community/lemma-overloading

Assia Mahboubi (May 27 2020 at 20:53):

Thanks for the tip @Karl Palmskog . I have to go offline now, but I should be able to try this tomorrow.

Assia Mahboubi (May 28 2020 at 07:50):

@Karl Palmskog @Théo Zimmermann I am trying to follow the README of coq-community's templates. The text is very clear, but for how to write a meta.yml : should I proceed by imitation from one of the projects cited (like lemma-overloading?).

Karl Palmskog (May 28 2020 at 07:59):

@Assia Mahboubi yes, it's probably a good idea to start from meta.yml in lemma-overloading, change things as appropriate, and remove things you don't need (many entries are completely optional, such as doi)

Théo Zimmermann (May 28 2020 at 08:22):

We've recently introduced a complete reference of the available keys (ref.yml) but it isn't yet mentioned in the README.

Assia Mahboubi (May 28 2020 at 08:57):

Thanks! I saw it meanwhile, and I am writing a meta.yml right now based on ref.yml + the meta.yml found in lemma-overloading.

Assia Mahboubi (May 28 2020 at 09:02):

Unfortunately, it does not work, and there is no informative error message:

$ ../templates/generate.sh
Unable to parse yaml!
Unable to parse yaml!
Unable to parse yaml!
Unable to parse yaml!
Unable to parse yaml!
Unable to parse yaml!
Generating index.md...
Unable to parse yaml!
Generating README.md...
Unable to parse yaml!
Unable to parse yaml!

Assia Mahboubi (May 28 2020 at 09:03):

I am using ruby-mustache in case it is useful.

Théo Zimmermann (May 28 2020 at 09:05):

Too bad the error message is not better than this. I think the issue is the leading and trailing ---. It's only need for a YAML header in a Markdown file, not for a purely YAML file.

Assia Mahboubi (May 28 2020 at 09:07):

I have blindly copied lemma-overloading.

Assia Mahboubi (May 28 2020 at 09:07):

Removing them does not change the output.

Théo Zimmermann (May 28 2020 at 09:08):

OK. Let me try to run this locally with my own mustache installation, which is mustache-go, to see if I get a better error message.

Karl Palmskog (May 28 2020 at 09:08):

@Assia Mahboubi you can always run mustache standalone, e.g., as follows:

mustache meta.yml ../templates/coq.opam.mustache > coq-lemma-overloading.opam
mustache meta.yml ../templates/README.md.mustache > README.md

That might further pinpoint the problem.

Théo Zimmermann (May 28 2020 at 09:11):

There's an issue with your dependencies

Théo Zimmermann (May 28 2020 at 09:12):

It should be:

dependencies:
- opam:
    name: coq-coqeal
    version: '{>= "1.0.3"}'
  description: CoqEal version 1.0.3+
- opam:
    name: coq-mathcomp-real-closed
    version: '{>= "1.0.4"}'
  description: MathComp/Real-Closed version 1.0.4+
- opam:
    name: coq-mathcomp-bigenough
    version: '{>= "1.0.0"}'
  description: MathComp/Bigenough version 1.0.0+

Assia Mahboubi (May 28 2020 at 09:13):

Indeed, many thanks @Théo Zimmermann !

Théo Zimmermann (May 28 2020 at 09:13):

I've further edited my message to include the description fields, which are not really optional until coq-community/templates#27 is finished and merged.

Assia Mahboubi (May 28 2020 at 09:14):

Thanks @Karl Palmskog , standalone generation now works as well, as expected.

Théo Zimmermann (May 28 2020 at 09:14):

FTR, I think we should make the generate.sh script more robust to errors. Will report an issue about this.

Assia Mahboubi (May 28 2020 at 09:15):

Now of course, one issue is that it generated a file named coq-apery.opam, and not coq-mathcomp-apery.opam

Théo Zimmermann (May 28 2020 at 09:16):

You can either change shortname into mathcomp-apery or define the opam_name variable.

Assia Mahboubi (May 28 2020 at 09:17):

Oh great! I did not understand what shortname was about : it is what comes after the coq- prefix?

Enrico Tassi (May 28 2020 at 09:17):

@Assia Mahboubi I don't recall if we ever defined guidelines, but I think your project should be called coq-apery. Sure it uses mathcomp, but is not a mathcomp component or extension

Assia Mahboubi (May 28 2020 at 09:18):

@Enrico Tassi Indeed, I hesitated for the name

Assia Mahboubi (May 28 2020 at 09:19):

But I made my choice by imitating what was done for fourcolour

Enrico Tassi (May 28 2020 at 09:19):

(we have coq-mathcomp-oddorder, which I believe is a mistake...)

Théo Zimmermann (May 28 2020 at 09:19):

shortname is the repository name. The default opam name is created by prepending coq- to it, but this can be overridden.

Assia Mahboubi (May 28 2020 at 09:20):

Oh wait, not fourcolour but oddorder indeed. I had a look at fourcolour as well, but at the time I had not realized that local opam files were not the same as opam-coq-archive. And the name field in this opam is coq-mathcomp-fourcolor. Now I am completely lost...

Enrico Tassi (May 28 2020 at 09:20):

Yep, it is my personal opinion, maybe we can discuss this at the next MC call.

Christian Doczkal (May 28 2020 at 09:21):

I agree with @Enrico Tassi , and my own projects follow his suggestion (as does indeed fourcolor)

Assia Mahboubi (May 28 2020 at 09:23):

So shortname is the repository name, and what is name?

Karl Palmskog (May 28 2020 at 09:25):

fullname is basically the "display name", used as README header, etc.

Théo Zimmermann (May 28 2020 at 09:25):

But it is called fullname. There is no name AFAICT.

Enrico Tassi (May 28 2020 at 09:26):

I think you found a bug in that opam file. When you put an opam file in the achive, the package name and version are taken from the directory in which the file is, not the fields name/version it may contain.

Assia Mahboubi (May 28 2020 at 09:26):

Anyway, @Enrico Tassi I could not find guidelines in mathcomp and it is probably a good idea to define and document some. I will thus make a pause with this until then.

Théo Zimmermann (May 28 2020 at 09:26):

Our own opam template does not contain such a name field BTW.

Assia Mahboubi (May 28 2020 at 09:27):

@Théo Zimmermann here is the infamous line.

Théo Zimmermann (May 28 2020 at 09:27):

Yep, I saw it ;-)

Assia Mahboubi (May 28 2020 at 09:43):

But meanwhile I still have a few questions regarding the templates: the generated .opam file still does not have the url and the checksum. And I do not see where I could have passed the relevant information for such fields to have been included hence my questions:

• are these generated .opam for CI purpose only?
• did I miss a way to generate the one for packaging purpose?
• or is the packaging one to be written by manual edition of the CI one?
• conversely, if I start with an . opam file for the purpose of packaging, can this same file but used for the purpose of CI?

Théo Zimmermann (May 28 2020 at 09:44):

They are generated mostly for CI purpose. They also allow one to opam install directly from the repository. Yes, at the current time, you still need to edit the file manually for packaging purpose but we'd like to automate that.

Karl Palmskog (May 28 2020 at 09:49):

one example of a generated .opam file and its edited archive counterpart: https://raw.githubusercontent.com/coq-community/buchberger/master/coq-buchberger.opam https://raw.githubusercontent.com/coq/opam-coq-archive/master/released/packages/coq-buchberger/coq-buchberger.8.11.0/opam -- here's the output of diff opam coq-buchberger.opam:

2a3
> version: "dev"
18c19
<   "coq" {>= "8.7" & < "8.12~"}
---
>   "coq" {(>= "8.7" & < "8.12~") | (= "dev")}
28d28
<   "date:2020-05-27"
34,38d33
<
< url {
<   src: "https://github.com/coq-community/buchberger/archive/v8.11.0.tar.gz"
<   checksum: "sha512=a048ee35574090d2ffa6b8c6a5e4379bb5f7699e0b84c1c4781fb624d151faca02eb9122bae2d21296ba6dbe57adb116edaa1255a5475b1cbafe89d33d364a05"
< }

Assia Mahboubi (May 28 2020 at 09:53):

Many thanks again @Karl Palmskog @Théo Zimmermann . So in principle, I could use the same file for both, if I do not want the CI to test dev , right?

Karl Palmskog (May 28 2020 at 09:56):

if you only want to keep the same opam file as in the archive and not use CI, that works, but be aware that it also prevents local pinning (cloning and then installing locally using opam)

Assia Mahboubi (May 28 2020 at 09:57):

I want to use CI, but not necessarily on dev.

Assia Mahboubi (May 28 2020 at 09:58):

Is it the presence of an url field which prevents local pinning?

Karl Palmskog (May 28 2020 at 09:58):

wait, I don't think I understand what dev means here? You mean you want to use CI, but not via opam? I guess Nix CI will still work

Assia Mahboubi (May 28 2020 at 09:58):

I want to use CI via opam indeed.

Karl Palmskog (May 28 2020 at 09:58):

Assia Mahboubi said:

Is it the presence of an url field which prevents local pinning?

right, to my knowledge the url stanza can't be ignored

Théo Zimmermann (May 28 2020 at 09:58):

I think @Assia Mahboubi is saying no need to test the dev version of Coq.

Assia Mahboubi (May 28 2020 at 09:59):

Yes, that's what I mean.

Théo Zimmermann (May 28 2020 at 09:59):

In this case, the only difference is that your local opam file will not contain the | (= "dev") part.

Théo Zimmermann (May 28 2020 at 09:59):

But the version: "dev" part is still required because it is the version of your package.

Karl Palmskog (May 28 2020 at 10:00):

right, specifying version: "dev" in the opam file in the repo usually prevents mixing up Coq opam repo versions of the same project in CI (has happened to me)

Assia Mahboubi (May 28 2020 at 10:03):

Ok, thanks a lot for the patient explanations, it is starting to become clearer.

Notification Bot (May 28 2020 at 10:24):

This topic was moved by Théo Zimmermann to #Coq devs & plugin devs > Keeping opam packages in sync.

Last updated: Sep 26 2023 at 12:02 UTC