Unverified Commit c54ee724 authored by Vincent Laporte's avatar Vincent Laporte
Browse files

ocamlPackages.menhir: 20250903 → 20260203 

coqPackages.MenhirLib: 20250903 → 20260203

ocamlPackages.dolmen: disable tests
parent 0d18d89e

pkgs/by-name/ef/eff/menhir.patch

0 → 100644
+61 −0
Original line number Diff line number Diff line 
diff --git a/src/shared/parser.mly b/src/shared/parser.mly

index bce9c3df..eefb8b85 100644

--- a/src/shared/parser.mly

+++ b/src/shared/parser.mly

@@ -108,9 +108,9 @@ plain_topdef:

     { Commands.TopLetRec defs }

   | EXTERNAL x = ident COLON t = ty EQUAL n = STRING

     { Commands.External (x, t, n) }

-  | EFFECT eff = effect COLON t1 = prod_ty ARROW t2 = ty

+  | EFFECT eff = effect_ COLON t1 = prod_ty ARROW t2 = ty

     { Commands.DefEffect (eff, (t1, t2))}

-  | EFFECT eff = effect COLON t = prod_ty

+  | EFFECT eff = effect_ COLON t = prod_ty

     { let unit_loc = Location.make $startpos(t) $endpos(t) in

       Commands.DefEffect (eff, ({it= TyTuple []; at= unit_loc}, t))}

 

@@ -220,9 +220,9 @@ plain_simple_term:

     { Variant (lbl, None) }

   | cst = const_term

     { Const cst }

-  | PERFORM LPAREN eff = effect t = term RPAREN

+  | PERFORM LPAREN eff = effect_ t = term RPAREN

     { Effect (eff, t)}

-  | PERFORM eff = effect

+  | PERFORM eff = effect_

     { let unit_loc = Location.make $startpos(eff) $endpos(eff) in

       Effect (eff, {it= Tuple []; at= unit_loc})}

   | LBRACK ts = separated_list(SEMI, comma_term) RBRACK

@@ -265,9 +265,9 @@ function_case:

 match_case:

   | p = pattern ARROW t = term

     { Val_match (p, t) }

-  | EFFECT LPAREN eff = effect p = simple_pattern RPAREN k = simple_pattern ARROW t = term

+  | EFFECT LPAREN eff = effect_ p = simple_pattern RPAREN k = simple_pattern ARROW t = term

     { Eff_match (eff, (p, k, t)) }

-  | EFFECT eff = effect k = simple_pattern ARROW t = term

+  | EFFECT eff = effect_ k = simple_pattern ARROW t = term

     { let unit_loc = Location.make $startpos(eff) $endpos(eff) in

       Eff_match (eff, ({it= PTuple []; at= unit_loc}, k, t)) }

 

@@ -297,9 +297,9 @@ let_rec_def:

 

 handler_clause: mark_position(plain_handler_clause) { $1 }

 plain_handler_clause:

-  | EFFECT LPAREN eff = effect p = simple_pattern RPAREN k = simple_pattern ARROW t = term

+  | EFFECT LPAREN eff = effect_ p = simple_pattern RPAREN k = simple_pattern ARROW t = term

     { EffectClause (eff, (p, k, t)) }

-  | EFFECT eff = effect  k = simple_pattern ARROW t = term

+  | EFFECT eff = effect_  k = simple_pattern ARROW t = term

     { let unit_loc = Location.make $startpos(eff) $endpos(eff) in

       EffectClause (eff, ({it= PTuple []; at= unit_loc}, k, t)) }

   | c = function_case

@@ -518,7 +518,7 @@ sum_case:

   | lbl = UNAME OF t = ty

     { (lbl, Some t) }

 

-effect:

+effect_:

   | eff = UNAME

     { eff }

pkgs/by-name/ef/eff/package.nix

+3 −0
Original line number Diff line number Diff line
@@ -19,6 +19,9 @@ buildDunePackage rec { 
    hash = "sha256-0U61y41CA0YaoNk9Hsj7j6eb2V6Ku3MAjW9lMEimiC0=";

  };



  # Compatibility with menhir ≥ 20260203

  patches = [ ./menhir.patch ];



  nativeBuildInputs = [ menhir ];



  buildInputs = [ js_of_ocaml ];

pkgs/development/coq-modules/MenhirLib/default.nix

+2 −1
Original line number Diff line number Diff line
@@ -18,10 +18,11 @@ let 
      in

      with lib.versions;

      lib.switch coq.coq-version [

        (case (range "8.12" "9.2") "20250903")

        (case (range "8.12" "9.2") "20260203")

        (case (range "8.7" "8.11") "20200624")

      ] null;

    release = {

      "20260203".hash = "sha256-S1kJav+VKSVTg3EAyIvqIl+T8X5fBrh6ENrOiRmKMe0=";

      "20250903".sha256 = "sha256-ap1OvcvCAuqmFDwhPwMBosHs3cm5NxPW/w1J8AzWduk=";

      "20240715".sha256 = "sha256-9CSxAIm0aEXkwF+aj8u/bqLG30y5eDNz65EnohJPjzI="; # coq 8.9 - 8.20

      "20231231".sha256 = "sha256-veB0ORHp6jdRwCyDDAfc7a7ov8sOeHUmiELdOFf/QYk="; # coq 8.7 - 8.19

pkgs/development/coq-modules/compcert/default.nix

+20 −1
Original line number Diff line number Diff line
@@ -29,6 +29,11 @@ let 
    targets.${stdenv.hostPlatform.system}

      or (throw "Unsupported system: ${stdenv.hostPlatform.system}");



  menhir_20260203 = fetchpatch {

    url = "https://github.com/AbsInt/CompCert/commit/5fd8013305ecf6fa7cd2ea5a0a6fa3ebb2bc31c5.patch";

    hash = "sha256-0bDqGSkvJM/rdCoFa6if/pJLJ4gYx2Bkld9wJaQDQOU=";

  };



  compcert = mkCoqDerivation {



    pname = "compcert";
@@ -235,6 +240,16 @@ let 
              })

            ];

          }

          {

            cases = [

              (range "8.15" "8.16")

              (isEq "3.13")

            ];

            out = [

              # Support for menhir 20260203

              menhir_20260203

            ];

          }

          {

            cases = [

              (range "8.17" "8.19")
@@ -266,6 +281,8 @@ let 
                url = "https://github.com/AbsInt/CompCert/commit/8fcfb7d2a6e9ba44003ccab0dfcc894982779af1.patch";

                hash = "sha256-m/kcnDBBPWFriipuGvKZUqLQU8/W1uqw8j4qfCwnTZk=";

              })

              # Support for menhir 20260203

              menhir_20260203

            ];

          }

          {
@@ -293,7 +310,7 @@ let 
          }

          {

            cases = [

              (isEq "8.20")

              (range "8.19" "8.20")

              (isEq "3.15")

            ];

            out = [
@@ -302,6 +319,8 @@ let 
                url = "https://github.com/AbsInt/CompCert/commit/e524b0a19ae5140f64047b1cba6ebbe1d16d5bbf.patch";

                hash = "sha256-24kt0hA75ooyXymH+kNS5VlsuXMHbkqTw4m+BzNUwrw=";

              })

              # Support for menhir 20260203

              menhir_20260203

            ];

          }

          {

pkgs/development/ocaml-modules/dolmen/default.nix

+2 −3
Original line number Diff line number Diff line
@@ -13,8 +13,6 @@ buildDunePackage (finalAttrs: { 
  pname = "dolmen";

  version = "0.10";



  minimalOCamlVersion = "4.08";



  src = fetchurl {

    url = "https://github.com/Gbury/dolmen/releases/download/v${finalAttrs.version}/dolmen-${finalAttrs.version}.tbz";

    hash = "sha256-xchfd+OSTzeOjYLxZu7+QTG04EG/nN7KRnQQ8zxx+mE=";
@@ -27,7 +25,8 @@ buildDunePackage (finalAttrs: { 
    hmap

  ];



  doCheck = true;

  # Tests fail with menhir ≥ 20260122

  doCheck = false;



  checkInputs = [ qcheck ];