Stream: Coq users

Topic: My first Coq opam package


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Assia Mahboubi (May 27 2020 at 15:33):

Is there anything else I should expect from the Makefile?

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (May 27 2020 at 15:45):

For a non .dev version you need the url

view this post on Zulip 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"
}

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Enrico Tassi (May 27 2020 at 15:51):

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

view this post on Zulip Théo Zimmermann (May 27 2020 at 15:52):

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

view this post on Zulip Enrico Tassi (May 27 2020 at 15:53):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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...)

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Assia Mahboubi (May 27 2020 at 17:59):

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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Cyril Cohen (May 27 2020 at 19:10):

The local opam file already serves the CI purposes

view this post on Zulip Karl Palmskog (May 27 2020 at 19:11):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?).

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:03):

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

view this post on Zulip 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.

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:07):

I have blindly copied lemma-overloading.

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:07):

Removing them does not change the output.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 28 2020 at 09:11):

There's an issue with your dependencies

view this post on Zulip 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+

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:13):

Indeed, many thanks @Théo Zimmermann !

view this post on Zulip 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.

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:14):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 28 2020 at 09:16):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:18):

@Enrico Tassi Indeed, I hesitated for the name

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:19):

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

view this post on Zulip Enrico Tassi (May 28 2020 at 09:19):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Enrico Tassi (May 28 2020 at 09:20):

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

view this post on Zulip Christian Doczkal (May 28 2020 at 09:21):

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

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:23):

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

view this post on Zulip Karl Palmskog (May 28 2020 at 09:25):

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

view this post on Zulip Théo Zimmermann (May 28 2020 at 09:25):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 28 2020 at 09:26):

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

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:27):

@Théo Zimmermann here is the infamous line.

view this post on Zulip Théo Zimmermann (May 28 2020 at 09:27):

Yep, I saw it ;-)

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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"
< }

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:57):

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

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:58):

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

view this post on Zulip 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

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:58):

I want to use CI via opam indeed.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 28 2020 at 09:58):

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

view this post on Zulip Assia Mahboubi (May 28 2020 at 09:59):

Yes, that's what I mean.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Assia Mahboubi (May 28 2020 at 10:03):

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

view this post on Zulip 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: Feb 06 2023 at 12:04 UTC