GNU bug report logs - #73236
[PATCH 0/2] gnu: Add coq-actris.

Previous Next

Full log

View this message in rfc822 format

From: Arnaud Daby-Seesaram <ds-ac <at> nanein.fr>
To: 73236 <at> debbugs.gnu.org
Cc: Antero Mejr <mail <at> antr.me>, pukkamustard <at> posteo.net, julien <at> lepiller.eu
Subject: [bug#73236] [PATCH 0/2] gnu: Add coq-actris.
Date: Wed, 09 Oct 2024 14:18:42 +0200

[Message part 1 (text/plain, inline)]

Hi Antero,

Thank you for your patches; I apologise for the response delay.

You will find a quick review below.

- Build: using your patch, both coq-iris and coq-actris can be
  successfully built (I only tried on a x86-64 machine with --rounds=3
  at the moment).

  However, I have a few questions:

  + I do not understand why COQTOP has to be specified in the
    #:make-flags.

  + Tests indeed fail if I switch #:tests? to #t.

    However, when I let the main build phase run the tests, they all
    seem to pass.  Do you experience the same result?
    If so, it could be worth it to (at least temporarily) allow tests in
    the main build phase (as is done in stdpp for example) and better
    understand where the issues come from.

  + Open question: would it be appropriate to split coq-iris across
    several outputs (main output for Iris, heap-lang, deprecated and
    unstable)?

  NB: I have not had the time to look at why there is a need to replace
      the install phase in coq-actris yet.

- Licenses: the licenses are correct.

- Home pages:
  + Iris: Ok.
  + Actris: you used a link to the GitLab repository.
    https://iris-project.org/actris/ might be more appropriate.

- Description fields:
  Descriptions are are usually phrased as "X is ...", where "X" is the
  name of the project.  Could you please rephrase the description in
  this style?

  Note: the Opam file of Iris reads "Iris is ..." too if you need a
  reference text.

- Documentation:
  It is very nice that you build and install iris.pdf.

  Do you think that adding a `native-search-paths' field to `coq-iris'
  (for variables "GUIX_TEXMF" and "BIBINPUTS") would be interesting?
  This way, `tex/iris.sty' and `tex/bib.bib' (maybe renamed into
  iris.bib) would be made available to TeX installations?


Sorry if writing my review as a list reads a bit cold (this is not my
intention); I just wanted to be as organised as possible.

Overall, thank you for you patches.  It would be nice to see
Iris-related stuff in Guix (and more generally more movement in the
OCaml/Coq worlds) :).

Best regards,

-- 
Arnaud

[signature.asc (application/pgp-signature, inline)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.