What is the tag for menhir for coq 8.12 when installing it with opam install -y?

Miscellaneous
1

I want to install opam menhir but make the install explicit for coq 8.12 to make my script explicit + robust to installation.

But when I ask it to show me it show the dev tag, which I assume might change at any point and make the install brittle. The project is hosted in gitlab and it doesn’t seem it lets me make a git issue here so asking here. From the available options is dev actually robust/stable? I don’t want future installs to break:

(iit_synthesis) brando9~ $ opam install -y menhir

[NOTE] Package menhir is already installed (current version is dev).
(iit_synthesis) brando9~ $
(iit_synthesis) brando9~ $ opam show menhir

<><> menhir: information on all versions ><><><><><><><><><><><><><><><><><><><>
name                   menhir
all-installed-versions 20190626 [coq-8.10]  dev [coq-8.12]
all-versions           20120123  20130116  20130911  20140422  20141215  20150914  20150921  20151005  20151012  20151023  20151026  20151030
                       20151103  20151112  20160303  20160504  20160526  20160808  20160825  20161114  20161115  20170101  20170418  20170509
                       20170607  20170712  20171013  20171206  20171222  20180528  20180530  20180703  20180905  20181006  20181026  20181113
                       20190613  20190620  20190626  20190924  20200123  20200211  20200525  20200612  20200619  20200624  20201122  20201201
                       20201214  20201216  20210310  20210419  20210929  20211012  20211125  20211128  20211230  20220210  dev

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>
version     dev
repository  coq-extra-dev
source-hash 98f5c17e
url.src     "git+https://gitlab.inria.fr/fpottier/menhir.git#master"
homepage    "http://gitlab.inria.fr/fpottier/menhir"
bug-reports "menhir@inria.fr"
dev-repo    "git+https://gitlab.inria.fr/fpottier/menhir.git"
authors     "François Pottier <francois.pottier@inria.fr>"
            "Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr>"
maintainer  "francois.pottier@inria.fr"
depends     "ocaml" {>= "4.02.3"}
            "dune" {>= "2.2.0"}
            "menhirLib" {= version}
            "menhirSdk" {= version}
synopsis    An LR(1) parser generator

e.g. I think this works for me in coq 8.10 which seems like a more reliable tag:

opam pin -y add menhir 20190626

cross: What is the tag for menhir for coq 8.12 when instlaling it with opam install -y? - Stack Overflow

2

Does Coq use menhir? I’d expect not. You should not use dev for reproducible results, but any other release should be reproducible.

Also, if you want stable results, you should probably disable the coq-extra-dev opam repository.

3

Coq 8.12 was mostly tested with menhir 20190626 , you can see this in the Docker file:

So that version is a good bet, but as Paolo points out, it depends on what menhir user you are interested in.

1 Like
4

command I ran:

# dev seems fine but scary to use dev tag: question for alternative: https://stackoverflow.com/questions/75465305/what-is-the-tag-for-menhir-for-coq-8-12-when-installing-it-with-opam-install-y
#opam install -y menhir
opam pin add -y menhir 20190626
# run bellow in case above break when using the intended coq switch
#opam install -y menhir=dev

output successful:

(metalearning_gpu) brando9~/proverbot9001/deps/StructTact $ opam install -y menhir 20190626
opam: PACKAGES... arguments: Package name "20190626" should contain at least
      one letter
Usage: opam install [OPTION]... [PACKAGES]...
Try `opam install --help' or `opam --help' for more information.
(metalearning_gpu) brando9~/proverbot9001/deps/StructTact $ opam pin add -y menhir 20190626

menhir is now pinned to version 20190626

The following actions will be performed:
  ⊘ remove    menhirLib dev              [conflicts with menhir]
  ⊘ remove    menhirSdk dev              [conflicts with menhir]
  ↘ downgrade menhir    dev to 20190626*
===== ↘ 1   ⊘ 2 =====

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⊘ removed   menhir.dev
⊘ removed   menhirLib.dev
⊘ removed   menhirSdk.dev
⬇ retrieved menhir.20190626  (cached)
∗ installed menhir.20190626
Done.
# Run eval $(opam env) to update the current shell environment
(metalearning_gpu) brando9~/proverbot9001/deps/StructTact $
(metalearning_gpu) brando9~/proverbot9001/deps/StructTact $ eval $(opam env)
1 Like