menhir issueshttps://gitlab.inria.fr/fpottier/menhir/-/issues2024-03-18T19:38:10+01:00https://gitlab.inria.fr/fpottier/menhir/-/issues/74Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.012024-03-18T19:38:10+01:00TETLEY RomainPlease pick the version you prefer for Coq 8.19 in Coq Platform 2024.01The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be...The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that the opam package we are currently testing in Coq Platform CI **works fine** with Coq `8.19.0`.
Coq Platform CI is currently testing opam package `coq-menhirlib.20231231`
from official repository https://coq.inria.fr/opam/released/packages/coq-menhirlib/coq-menhirlib.20231231/opam.
**In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.**
In case you would prefer to see an updated or an older version in the upcoming Coq Platform `2024.01`, please inform us as soon as possible and before **March 31st, 2024**!
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.19~2024.01+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.19~2024.01+beta1.sh) which already supports Coq version `8.19.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
In case you want to select a different version, please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/405https://gitlab.inria.fr/fpottier/menhir/-/issues/73Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.102023-10-05T18:09:29+02:00TETLEY RomainPlease pick the version you prefer for Coq 8.18 in Coq Platform 2023.10The Coq team released Coq `8.18.0` on September 7th, 2023.
The corresponding Coq Platform release `2023.10` should be released before **November 30th, 2023**.
It can be delayed in case of difficulties until January 15th, 2023, but this s...The Coq team released Coq `8.18.0` on September 7th, 2023.
The corresponding Coq Platform release `2023.10` should be released before **November 30th, 2023**.
It can be delayed in case of difficulties until January 15th, 2023, but this should be an exception.
This issue is to inform you that the opam package we are currently testing in Coq Platform CI **works fine** with Coq `8.18.0`.
Coq Platform CI is currently testing opam package `coq-menhirlib.20230608`
from official repository https://coq.inria.fr/opam/released/packages/coq-menhirlib/coq-menhirlib.20230608/opam.
**In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.**
In case you would prefer to see an updated or an older version in the upcoming Coq Platform `2023.10`, please inform us as soon as possible and before **October 31st, 2023**!
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.18+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.18+beta1.sh) which already supports Coq version `8.18.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
In case you want to select a different version, please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/372https://gitlab.inria.fr/fpottier/menhir/-/issues/72Can't use `--merge-errors`2023-10-04T18:46:27+02:00Vincent TourneurCan't use `--merge-errors`Hello,
I am trying to use the option `--merge-errors`, as described in the documentation (https://gallium.inria.fr/~fpottier/menhir/manual.html#sec76).
Menhir gives me a invalid usage error message:
```
$ menhir --merge-errors file1.me...Hello,
I am trying to use the option `--merge-errors`, as described in the documentation (https://gallium.inria.fr/~fpottier/menhir/manual.html#sec76).
Menhir gives me a invalid usage error message:
```
$ menhir --merge-errors file1.messages --merge-errors file2.messages
Usage: menhir <options> <filenames>
```
I also tried using it with only one `--merge-errors`, which gives an uncaught exception:
```
$ menhir --merge-errors file1.messages file2.messages
Fatal error: exception Invalid_argument("Filename.chop_suffix")
```
Thank youhttps://gitlab.inria.fr/fpottier/menhir/-/issues/71morally-incorrect "unused variable" warnings2023-04-01T20:10:40+02:00SCHERER Gabrielmorally-incorrect "unused variable" warningsfoo.mly:
```
%token TOKEN
%start start
%type <Lexing.position * Lexing.position> start
%%
start:
| tok=TOKEN { $loc(tok) }
;
```
```
$ menhir --ocamlc "ocamlc -w +27" --infer /tmp/foo.mly
File "/tmp/foo.mly", line 9, characters 2-5:
...foo.mly:
```
%token TOKEN
%start start
%type <Lexing.position * Lexing.position> start
%%
start:
| tok=TOKEN { $loc(tok) }
;
```
```
$ menhir --ocamlc "ocamlc -w +27" --infer /tmp/foo.mly
File "/tmp/foo.mly", line 9, characters 2-5:
Warning 27 [unused-var-strict]: unused variable tok.
```
Menhir generates code that does not use the variable `tok` (which denotes the semantic value of the token), but the semantic action does use the variable.
I think that the code generator for `$macro(foo)` should be tuned to include an `ignore foo` call, to silence this warning.
One can of course disable the warning globally for the whole file (menhir could do it by adding a well-chosen attribute, or I could do it by tweaking the build system), but this risks silencing warnings in the semantic actions that do in fact correspond to code-quality issues that the users wants to know about.
(I wondered if this was hopeless because Menhir generates too many unused-variable warnings anyway. But I think not: I observed the present issue when modifying the Menhir grammar in the OCaml compiler, which means that it currently compiles fine with the warning enabled. This is evidence that large, non-trivial Menhir grammars can compile with this flag enabled, at least when using the --table backend.)https://gitlab.inria.fr/fpottier/menhir/-/issues/70--interpret-show-cst seems broken2023-03-30T14:06:07+02:00SCHERER Gabriel--interpret-show-cst seems broken```
$ menhir --version
menhir, version 20220210
$ menhir --interpret-show-cst ~/Prog/menhir/test/static/good/calc.mly
Fatal error: exception File "src/back.ml", line 39, characters 6-12: Assertion failed
```
I have not been able to use ...```
$ menhir --version
menhir, version 20220210
$ menhir --interpret-show-cst ~/Prog/menhir/test/static/good/calc.mly
Fatal error: exception File "src/back.ml", line 39, characters 6-12: Assertion failed
```
I have not been able to use `--interpret-show-cst`, even with older versions of Menhir. My assumption would be that it behaves like `--interpret`, it creates an interactive prompt, but it shows parse derivations on acceptance. In practice either I get an assertion failure as the above, or menhir silently returns immediately (on older versions such as 20210419).https://gitlab.inria.fr/fpottier/menhir/-/issues/69Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.032023-02-28T21:53:37+01:00Michael SoegtropPlease pick the version you prefer for Coq 8.17 in Coq Platform 2023.03The Coq team released Coq `8.17+rc1` on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023.
The corresponding Coq Platform release `2023.03` should be released before **April 14th, 2023**.
It can be delayed in cas...The Coq team released Coq `8.17+rc1` on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023.
The corresponding Coq Platform release `2023.03` should be released before **April 14th, 2023**.
It can be delayed in case of difficulties until June 30, 2023, but this should be an exception.
This issue is to inform you that the opam package we are currently testing in Coq Platform CI **works fine** with Coq `8.17+rc1`.
Coq Platform CI is currently testing opam package `coq-menhirlib.20220210`
from official repository https://coq.inria.fr/opam/released/packages/coq-menhirlib/coq-menhirlib.20220210/opam.
**In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.**
In case you would prefer to see an updated or an older version in the upcoming Coq Platform `2023.03`, please inform us as soon as possible and before **March 21st, 2023**!
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.17~2023.03+preview1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.17~2023.03+preview1.sh) which already supports Coq version `8.17+rc1` and contains already working (possibly patched / commit pinned) Coq Platform packages.
In case you want to select a different version, please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/335https://gitlab.inria.fr/fpottier/menhir/-/issues/68Type inference makes module aliases declared in preamble leak in the .mli2023-02-03T16:49:24+01:00Thierry MartinezType inference makes module aliases declared in preamble leak in the .mliWhen an alias for a module is declared in the preamble, if a type defined in this module is used in the return type of a starting symbol, then the alias is preferred in the `.mli` to refer to this type rather than the original module nam...When an alias for a module is declared in the preamble, if a type defined in this module is used in the return type of a starting symbol, then the alias is preferred in the `.mli` to refer to this type rather than the original module name, whereas the alias is not defined in the `.mli`.
In the following example, `some_module.ml` is:
```ocaml
type t = C
```
The following grammar generates a `.mli` that fails to compile, giving the type `M.t` for the return value of `s`, where `M` is unbound.
```ocaml
%{
module M = Some_module
%}
%token T
%type <Some_module.t> s
%start s
%%
s:
| T
{ Some_module.C }
```https://gitlab.inria.fr/fpottier/menhir/-/issues/67OCaml lexer is not up-to-date2022-11-18T13:39:05+01:00POTTIER Francoisfrancois.pottier@inria.frOCaml lexer is not up-to-dateMenhir's lexer does not recognize OCaml string literals of the form `{a|...|a}`. This has been reported by Demi Marie Obenour.
At the very least, Menhir's lexer should be updated so as to remain in sync with OCaml's lexer.
More ambitio...Menhir's lexer does not recognize OCaml string literals of the form `{a|...|a}`. This has been reported by Demi Marie Obenour.
At the very least, Menhir's lexer should be updated so as to remain in sync with OCaml's lexer.
More ambitiously, this may be a good time to think about splitting the lexer, that is, distinguishing the lexer that is used outside semantic actions and the lexer that is used inside semantic actions. The former is Menhir-specific; the latter could conceivably depend on the target language (in a future version of Menhir with multiple target languages).POTTIER Francoisfrancois.pottier@inria.frPOTTIER Francoisfrancois.pottier@inria.frhttps://gitlab.inria.fr/fpottier/menhir/-/issues/66Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.092022-09-06T15:33:02+02:00Michael SoegtropPlease pick the version you prefer for Coq 8.16 in Coq Platform 2022.09The Coq team released Coq `8.16+rc1` on June 01, 2022.
The corresponding Coq Platform release `2022.09` should be released before **September 15, 2022**.
It can be delayed in case of difficulties until October 15, 2022, but this should b...The Coq team released Coq `8.16+rc1` on June 01, 2022.
The corresponding Coq Platform release `2022.09` should be released before **September 15, 2022**.
It can be delayed in case of difficulties until October 15, 2022, but this should be an exception.
This issue is to inform you that the opam package we are currently testing in Coq Platform CI **works fine** with Coq `8.16+rc1`.
Coq Platform CI is currently testing opam package `coq-menhirlib.20220210`
from official repository https://coq.inria.fr/opam/released/packages/coq-menhirlib/coq-menhirlib.20220210/opam.
**In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.**
In case you would prefer to see an updated or an older version in the upcoming Coq Platform `2022.09`, please inform us as soon as possible and before **August 31, 2022**!
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.16+rc1~2022.09~preview1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.16~2022.09~preview1.sh) which already supports Coq version `8.16+rc1` and contains already working (possibly patched / commit pinned) Coq Platform packages.
In case you want to select a different version, please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/274https://gitlab.inria.fr/fpottier/menhir/-/issues/65[wish] first class token precedence2022-03-17T09:55:46+01:00TASSI Enrico[wish] first class token precedenceIt would be nice if Menhir could generate an OCaml value representing the precedence of tokens.
I'd like to then generate (automatically) that part of the the documentation of my language.
Since tokens can carry a value, I'd be happy to...It would be nice if Menhir could generate an OCaml value representing the precedence of tokens.
I'd like to then generate (automatically) that part of the the documentation of my language.
Since tokens can carry a value, I'd be happy to say `%example TOKEN "foo"` to ease the creation of that value.
Alternatively, Menhir could take that piece of info out of an OCaml value crafted by the user, eg
```
%precedence <
[ Nonassoc [ TOK1 ]
| Right [ TOK2 "foo" ; TOK3 ]
| ..
]
>
```
in place of
```
%nonassoc TOK1
%right TOK2 TOK3
```
One could define that concrete list in another file if he wishes to access it later.https://gitlab.inria.fr/fpottier/menhir/-/issues/64Fatal error: exception File "src/LRijkstraFast.ml", line 892, characters 10-1...2022-01-25T18:01:21+01:00TASSI EnricoFatal error: exception File "src/LRijkstraFast.ml", line 892, characters 10-16: Assertion failed```shell
$ git clone https://github.com/LPCIC/elpi.git -b adt/parser /tmp/elpi
$ cd /tmp/elpi
$ git describe
v1.13.7-75-g7c68669
$ opam list | grep menhir
menhir 20211230 An LR(1) parser generator
$ make complete
men...```shell
$ git clone https://github.com/LPCIC/elpi.git -b adt/parser /tmp/elpi
$ cd /tmp/elpi
$ git describe
v1.13.7-75-g7c68669
$ opam list | grep menhir
menhir 20211230 An LR(1) parser generator
$ make complete
menhir src/tokens.mly --base parser2 src/parser2.mly \
--list-errors > src/parser2Messages.auto.messages
...
Fatal error: exception File "src/LRijkstraFast.ml", line 892, characters 10-16: Assertion failed
```
The parser is super WIP, and probably I don't know what I'm doing, but this is what I get when I try to generate a template for the messages. If it helps debugging, the previous commit was working.https://gitlab.inria.fr/fpottier/menhir/-/issues/63Please pick the version you prefer for Coq 8.15 in Coq Platform 2022.022022-03-23T11:30:52+01:00Michael SoegtropPlease pick the version you prefer for Coq 8.15 in Coq Platform 2022.02The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an excep...The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.
This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.15.0.
Coq Platform CI is currently testing opam package `coq-menhirlib.20211230`
from official repository https://coq.inria.fr/opam/released/packages/coq-menhirlib/coq-menhirlib.20211230/opam.
In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.
In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2022.02, please inform us as soon as possible and before February 14, 2022!
The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.
In case you want to select a different version, please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/193https://gitlab.inria.fr/fpottier/menhir/-/issues/62Regression (in 2021-12-30 ?) concerning parse errors2022-02-10T18:58:41+01:00Andreas AbelRegression (in 2021-12-30 ?) concerning parse errorsConsider the following LBNF grammar, which can be translated to a menhir-grammar using `bnfc --ocaml-menhir` (https://github.com/BNFC/bnfc).
```
EInt. Exp1 ::= Integer; -- entrypoint
EPlus. Exp ::= Exp "+" Exp1;
```
The rule `EPlus` can...Consider the following LBNF grammar, which can be translated to a menhir-grammar using `bnfc --ocaml-menhir` (https://github.com/BNFC/bnfc).
```
EInt. Exp1 ::= Integer; -- entrypoint
EPlus. Exp ::= Exp "+" Exp1;
```
The rule `EPlus` can never fire, so running the parser on `1+2` will fail. However, the error message of menhir-2021-12-30 is worse than the one of e.g. menhir-2021-04-19 or ocamlyacc:
```
$ ocaml/TestTest <<< "1+2"
Parse error at 1.2-1.3
$ menhir-2021-04-19/TestTest <<< "1+2"
Parse error at 1.2-1.3
$ menhir-2021-12-30/TestTest <<< "1+2"
Fatal error: exception ParTest.MenhirBasics.Error
```
The somewhat simplified `.mly` file generated by `bnfc --ocaml-menhir` is this:
```ocaml
%{
open AbsTest
open Lexing
%}
%token SYMB1 /* + */
%token TOK_EOF
%token <int> TOK_Integer
%start pExp1 pExp
%type <AbsTest.exp> pExp1
%type <AbsTest.exp> pExp
%type <AbsTest.exp> exp1
%type <AbsTest.exp> exp
%type <int> int
%%
pExp1 : exp1 TOK_EOF { $1 }
| error { raise (BNFC_Util.Parse_error ($symbolstartpos, $endpos)) };
pExp : exp TOK_EOF { $1 }
| error { raise (BNFC_Util.Parse_error ($symbolstartpos, $endpos)) };
exp1 : int { EInt $1 };
exp : exp SYMB1 exp1 { EPlus ($1, $3) };
int : TOK_Integer { $1 };
```
Checking the [changelog](https://gitlab.inria.fr/fpottier/menhir/-/blob/ce71e652219bd4624e6702f20cb0896836447d84/CHANGES.md), it seems that the use of the `error` token is within the backward-compatible way:
> For grammars that use the `error` token in the limited way permitted by the simplified strategy, this makes no difference either. The simplified strategy makes the following requirement: the `error` token should always appear at the end of a production, whose semantic action should abort the parser by raising an exception.
All the generated code is in the attached tar file: [regression-2021-12-30.tgz](/uploads/22302dfd38bc257552210d1dae5d5fd7/regression-2021-12-30.tgz)https://gitlab.inria.fr/fpottier/menhir/-/issues/61Problem with type inference2022-01-03T19:50:56+01:00Frédéric BlanquiProblem with type inferenceHello François. Following your PR/issue on Lambdapi, I tried to fix it but I have a problem that seems related to Menhir. See https://github.com/Deducteam/lambdapi/pull/798. I would appreciate your help very much.Hello François. Following your PR/issue on Lambdapi, I tried to fix it but I have a problem that seems related to Menhir. See https://github.com/Deducteam/lambdapi/pull/798. I would appreciate your help very much.https://gitlab.inria.fr/fpottier/menhir/-/issues/60MenhirLib does not install .coq-native directories2022-01-20T17:15:06+01:00Guillaume MelquiondMenhirLib does not install .coq-native directoriesAs far as I can tell, the `install` rule of `coq-menhirlib/src/Makefile` does not install the `.coq-native` directory. As a consequence, it is impossible to compile a file that depends on MenhirLib using a native-enabled Coq. For example...As far as I can tell, the `install` rule of `coq-menhirlib/src/Makefile` does not install the `.coq-native` directory. As a consequence, it is impossible to compile a file that depends on MenhirLib using a native-enabled Coq. For example, I get the following error when compiling CompCert.
```
COQC cparser/Parser.v
File "./cparser/.coq-native/Ncompcert_cparser_Parser.native", line 4760, characters 15-77:
4760 | ((Obj.magic (NMenhirLib_Alphabet.Construct_NMenhirLib_Alphabet_Numbered_0_1((
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module NMenhirLib_Alphabet
Error: Native compiler exited with status 2
```
If so, my suggestion would be:
1. Add `conflicts: ["coq-native"]` to all the existing Opam packages for `coq-menhirlib`, so that it cannot be installed next to a native-enabled compiler.
2. Fix the `install` rule for the next release.https://gitlab.inria.fr/fpottier/menhir/-/issues/59Consider moving to a hosting platform with public feedback?2021-11-30T15:51:36+01:00Romain BeauxisConsider moving to a hosting platform with public feedback?I was lucky enough to have a contact who allowed me to register an account with this website, otherwise it is impossible to file public issues/PR with the project.
Perhaps it would be advisable to move the project to a place that allow...I was lucky enough to have a contact who allowed me to register an account with this website, otherwise it is impossible to file public issues/PR with the project.
Perhaps it would be advisable to move the project to a place that allows public feedback?
Thanks!https://gitlab.inria.fr/fpottier/menhir/-/issues/58How to handle dependencies with `--infer`2022-02-11T19:24:12+01:00Romain BeauxisHow to handle dependencies with `--infer`Hi,
I'm trying to convert liquidsoap to use `--infer` like recently suggested. However, we have dependencies from our `.mly` files to `.ml` files that `ocamlc` needs to see compiled before being able to run. For instance:
```
%start js...Hi,
I'm trying to convert liquidsoap to use `--infer` like recently suggested. However, we have dependencies from our `.mly` files to `.ml` files that `ocamlc` needs to see compiled before being able to run. For instance:
```
%start json
%type <Json_base.t> json
```
`menhir --depend` seems to output dependencies for compiles `.cm*` files, which is no use for this. Is there any other way to automatize dependency tracking in this case?https://gitlab.inria.fr/fpottier/menhir/-/issues/57Is menhir.20211125 compatible with ocaml 4.08, 4.09 and 4.10 ?2021-11-27T17:51:14+01:00Frédéric BlanquiIs menhir.20211125 compatible with ocaml 4.08, 4.09 and 4.10 ?See https://github.com/OCamlPro/alt-ergo/issues/492.See https://github.com/OCamlPro/alt-ergo/issues/492.https://gitlab.inria.fr/fpottier/menhir/-/issues/56Coq 8.14 warnings2021-09-28T10:42:28+02:00Xavier LeroyCoq 8.14 warningsNew warnings in Coq 8.14 are triggered both by .v files produced by Menhir, and by .v files from the Coq library coq-menhirlib.
Concerning the latter, here is a fix: https://github.com/AbsInt/CompCert/pull/415/commits/05514d7ef81dda3cbf...New warnings in Coq 8.14 are triggered both by .v files produced by Menhir, and by .v files from the Coq library coq-menhirlib.
Concerning the latter, here is a fix: https://github.com/AbsInt/CompCert/pull/415/commits/05514d7ef81dda3cbfa3cf5fe3f12d892fc1477f
I elected to use `Global Instance` instead of `[#export] Instance` because the latter is not supported before Coq 8.13.
Concerning Menhir-generated Coq files: `Instance` needs to be qualified as `Global Instance`, for the same reasons.https://gitlab.inria.fr/fpottier/menhir/-/issues/55Informative: pick of tag for upcoming release of Coq Platform for Coq 8.142021-11-15T09:42:14+01:00Michael SoegtropInformative: pick of tag for upcoming release of Coq Platform for Coq 8.14The Coq team released Coq 8.14+rc1 on September 17, 2021
and plans to release Coq 8.14.0 before October 31, 2021.
A corresponding Coq Platform releases should be released before November 30, 2021.
It can be dealyed in case of difficultie...The Coq team released Coq 8.14+rc1 on September 17, 2021
and plans to release Coq 8.14.0 before October 31, 2021.
A corresponding Coq Platform releases should be released before November 30, 2021.
It can be dealyed in case of difficulties until January 31, 2022, but this should be an exception.
This issue is to inform you that your latest tag does work fine with Coq 8.14+rc1.
Coq Platform currently uses the opam package 'coq-menhirlib.20210419'
from official repository https://coq.inria.fr/opam/released.
In case this is the version you want to see in Coq Platform, there is nothing to do for you - just close this issue.
In case you would prefer to see an updated version in the upcoming Coq Platform, please inform as as soon as possible!
Thanks!
P.S.: this issue has been created semi-automatically.
CC: https://github.com/coq/platform/issues/139