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

28 Views Asked by At

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 "[email protected]"
dev-repo    "git+https://gitlab.inria.fr/fpottier/menhir.git"
authors     "François Pottier <[email protected]>"
            "Yann Régis-Gianas <[email protected]>"
maintainer  "[email protected]"
depends     "ocaml" {>= "4.02.3"}
            "dune" {>= "2.2.0"}
            "menhirLib" {= version}
            "menhirSdk" {= version}
synopsis    An LR(1) parser generator

cross: https://coq.discourse.group/t/what-is-the-tag-for-menhir-for-coq-8-12-when-instlaling-it-with-opam-install-y/1889

1

There are 1 best solutions below

0
Charlie Parker On

source: https://coq.discourse.group/t/what-is-the-tag-for-menhir-for-coq-8-12-when-installing-it-with-opam-install-y/1889/3?u=brando90

Answer emilio gave:

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

github.com
coq/coq/blob/v8.12/dev/ci/docker/bionic_coq/Dockerfile
# CACHEKEY: "bionic_coq-v8.12-V2020-10-12-V1"
# ^^ Update when modifying this file.

FROM ubuntu:bionic
LABEL maintainer="[email protected]"

ENV DEBIAN_FRONTEND="noninteractive"

RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
        # Dependencies of the image, the test-suite and external projects
        m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip jq \
        # Dependencies of lablgtk (for CoqIDE)
        libgtksourceview-3.0-dev \
        # Dependencies of stdlib and sphinx doc
        texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
        python3-pip python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \
        # Dependencies of source-doc and coq-makefile
        texlive-science tipa

# More dependencies of the sphinx doc
This file has been truncated. show original
So that version is a good bet, but as Paolo points out, it depends on what menhir user you are interested in.

thus 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)