From 9c3b24cc90fb69613f6d4071b8c8fbbd7c22979e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 18 May 2020 17:32:21 +0200 Subject: [PATCH 1/8] port to coq-elpi 1.4 --- hb.elpi | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/hb.elpi b/hb.elpi index 71c193e61..4a3f92358 100644 --- a/hb.elpi +++ b/hb.elpi @@ -125,14 +125,16 @@ name-of-asset-decl (asset-record X _ _ _) X. name-of-asset-decl (asset-alias X _) X. pred argument->asset i:argument, o:asset-decl. -argument->asset (indt-decl (parameter Name Ty I)) (asset-parameter "T" Ty A) :- % TODO, take the name +argument->asset (indt-decl (parameter ID _ Ty I)) (asset-parameter ID Ty A) :- + coq.string->name ID Name, @pi-decl Name Ty a\ argument->asset (indt-decl (I a)) (A a). argument->asset (indt-decl (record Rid Ty Kid F)) (asset-record Rid Ty Kid F) :- !. -argument->asset (const-decl Id (some (fun _ _ Bo)) (some (prod Name Src Ty))) (asset-parameter "T" Src A) :- !, +argument->asset (const-decl Id (some (fun _ _ Bo)) (parameter ID _ Src Ty)) (asset-parameter ID Src A) :- !, + coq.id->name ID Name, @pi-decl Name Src a\ - argument->asset (const-decl Id (some (Bo a)) (some (Ty a))) (A a). -argument->asset (const-decl Id (some Bo) (some Ty)) (asset-alias Id Bo) :- !, + argument->asset (const-decl Id (some (Bo a)) (Ty a)) (A a). +argument->asset (const-decl Id (some Bo) (arity Ty)) (asset-alias Id Bo) :- !, std.assert! (var Ty) "Factories aliases should not be given a type". argument->asset X _ :- coq.error "Unsupported asset:" X. @@ -966,7 +968,7 @@ declare-class ML (indt ClassName) Factories :- std.do! [ (@pi-decl `T` {{Type}} t\ synthesize-fields t ML (RDecl t)), ClassDeclaration = - (parameter `T` {{ Type }} t\ + (parameter "T" explicit {{ Type }} t\ record "axioms" {{ Type }} "Class" (RDecl t)), std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped", coq.env.add-indt ClassDeclaration ClassName, @@ -1149,11 +1151,11 @@ declare-old-constant (some C) :- declare-old-constant _ :- true. pred main-begin-declare-builders i:context-decl. -main-begin-declare-builders (context-item _ _ none _\ context-item IDF _ (some _) _\ context-end) :- +main-begin-declare-builders (context-item _ _ _ none _\ context-item IDF _ _ (some _) _\ context-end) :- coq.error "factories cannot be given a body:" IDF. -main-begin-declare-builders (context-item _ _ none _\ context-item ID1 _ none _\ context-item ID2 _ _ _) :- +main-begin-declare-builders (context-item _ _ _ none _\ context-item ID1 _ _ none _\ context-item ID2 _ _ _ _) :- coq.error "only one factory is supported, got at least two" ID1 "and" ID2. -main-begin-declare-builders (context-item IDT T none t\ context-item IDF (F t) none _\ context-end) :- std.do! [ +main-begin-declare-builders (context-item IDT _ T none t\ context-item IDF _ (F t) none _\ context-end) :- std.do! [ Name is "Builders_" ^ {term_to_string {new_int}}, % TODO std.assert! (pi t\ F t = app[global GRA, t|_]) "a factory must be a name applied to the type variable", factory-alias->gref GRA GRF, From 98dca06e7ea7923c325e6653d823677d10115e52 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 19 May 2020 09:45:16 +0200 Subject: [PATCH 2/8] coq.unify* give a diagnostic --- hb.elpi | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/hb.elpi b/hb.elpi index 4a3f92358..9ec4d8e30 100644 --- a/hb.elpi +++ b/hb.elpi @@ -343,8 +343,9 @@ local-cs? TyTerm Struct :- pred get-canonical-mixins-of i:term, i:structure, o:list prop. get-canonical-mixins-of T S MSL :- std.do! [ get-structure-sort-projection S Sort, - coq.unify-eq T (app [Sort, ST]), - coq.unify-eq ST (app [_, _, C]), + std.assert-ok! (coq.unify-eq T (app [Sort, ST])) "HB: get-canonical-mixins-of: T = sort ST", + % Hum, this unification problem is not super trivial. TODO replace by something simpler + std.assert-ok! (coq.unify-eq ST (app [_, _, C])) "HB: get-canonical-mixins-of: ST = _ _ C", C = app [_, _ | MIL], std.map MIL (mixin-srcs T) MSLL, std.flatten MSLL MSL From be67ca7aed667976b35234327f4c50ec7b965614 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 19 May 2020 10:23:52 +0200 Subject: [PATCH 3/8] updating nix pkgs --- default.nix | 11 +++++++---- shell.nix | 16 +++++++++------- 2 files changed, 16 insertions(+), 11 deletions(-) diff --git a/default.nix b/default.nix index e517f7d16..d7483253c 100644 --- a/default.nix +++ b/default.nix @@ -1,9 +1,9 @@ {withEmacs ? false, nixpkgs ? (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/82b54d490663b6d87b7b34b9cfc0985df8b49c7d.tar.gz"; - sha256 = "12gpsif48g5b4ys45x36g4vdf0srgal4c96351m7gd2jsgvdllyf"; + url = "https://github.com/CohenCyril/nixpkgs/archive/7f59c094a0e5c8659856e611075fe88d6177830f.tar.gz"; + sha256 = "00cf4r8dqfx2hwlwaqb239h72m4s0wl97i98424xd4hki0vzifbi"; }), - coq-version ? "8.10", + coq-version ? "8.11", print-env ? false }: with import nixpkgs {}; @@ -15,7 +15,10 @@ let "8.11" = coqPackages_8_11; }."${coq-version}"; coq = myCoqPackages.coq; - coq-elpi = myCoqPackages.coq-elpi; + coq-elpi = myCoqPackages.coq-elpi.overrideAttrs(o: { + name = "coq8.11-elpi-784659c"; + src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/784659cbc4ced031b87fc9eda349162169f15084.tar.gz; + }); in stdenv.mkDerivation { name = "coq${coq.coq-version}-hierarchy-builder-dev"; diff --git a/shell.nix b/shell.nix index 37d4ae379..c33f19e2e 100644 --- a/shell.nix +++ b/shell.nix @@ -1,9 +1,9 @@ {withEmacs ? false, nixpkgs ? (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/82b54d490663b6d87b7b34b9cfc0985df8b49c7d.tar.gz"; - sha256 = "12gpsif48g5b4ys45x36g4vdf0srgal4c96351m7gd2jsgvdllyf"; + url = "https://github.com/CohenCyril/nixpkgs/archive/7f59c094a0e5c8659856e611075fe88d6177830f.tar.gz"; + sha256 = "00cf4r8dqfx2hwlwaqb239h72m4s0wl97i98424xd4hki0vzifbi"; }), - coq-version ? "8.10", + coq-version ? "8.11", print-env ? false }: with import nixpkgs {}; @@ -11,17 +11,19 @@ let pgEmacs = emacsWithPackages (epkgs: with epkgs.melpaStablePackages; [proof-general]); myCoqPackages = { - "8.7" = coqPackages_8_7; - "8.8" = coqPackages_8_8; - "8.9" = coqPackages_8_9; "8.10" = coqPackages_8_10; + "8.11" = coqPackages_8_11; }."${coq-version}"; coq = myCoqPackages.coq; + coq-elpi = myCoqPackages.coq-elpi.overrideAttrs (o: { + name = "coq8.11-elpi-784659c"; + src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/784659cbc4ced031b87fc9eda349162169f15084.tar.gz; + }); in stdenv.mkDerivation rec { name = "env"; env = buildEnv { name = name; paths = buildInputs; }; - buildInputs = [ coq myCoqPackages.coq-elpi ] + buildInputs = [ coq coq.ocaml coq.ocamlPackages.elpi coq-elpi ] ++ lib.optional withEmacs pgEmacs ++ [ pythonPackages.pygments ] ; shellHook = '' From d8a8b12e5c6cfe3109b8b28ce8495c4e60c12dde Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 19 May 2020 10:30:20 +0200 Subject: [PATCH 4/8] commenting out broken CI --- .travis.yml | 108 ++++++++++++++++++++++++++-------------------------- 1 file changed, 54 insertions(+), 54 deletions(-) diff --git a/.travis.yml b/.travis.yml index 31b62b2be..12872757b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -13,11 +13,11 @@ env: jobs: include: - - language: nix - env: - - COQ=8.10 - script: - - nix-build --argstr coq-version "${COQ}" + # - language: nix + # env: + # - COQ=8.10 + # script: + # - nix-build --argstr coq-version "${COQ}" - language: nix env: @@ -25,55 +25,55 @@ jobs: script: - nix-build --argstr coq-version "${COQ}" - - dist: bionic - language: minimal - services: - - docker - env: - - COQ=8.10 ELPI="install ${ELPI_810}" CMD="make && make install" - install: - - ./.travis/docker-install.sh - script: - - ./.travis/docker-test.sh - after_script: - - docker stop COQ + # - dist: bionic + # language: minimal + # services: + # - docker + # env: + # - COQ=8.10 ELPI="install ${ELPI_810}" CMD="make && make install" + # install: + # - ./.travis/docker-install.sh + # script: + # - ./.travis/docker-test.sh + # after_script: + # - docker stop COQ - - dist: bionic - language: minimal - services: - - docker - env: - - COQ=8.11 ELPI="install ${ELPI_811}" CMD="make && make install" - install: - - ./.travis/docker-install.sh - script: - - ./.travis/docker-test.sh - after_script: - - docker stop COQ + # - dist: bionic + # language: minimal + # services: + # - docker + # env: + # - COQ=8.11 ELPI="install ${ELPI_811}" CMD="make && make install" + # install: + # - ./.travis/docker-install.sh + # script: + # - ./.travis/docker-test.sh + # after_script: + # - docker stop COQ - - dist: bionic - language: minimal - services: - - docker - env: - - COQ=8.11 ELPI="install ${ELPI_811}" CMD="opam pin add coq-hierarchy-builder ." - install: - - ./.travis/docker-install.sh - script: - - ./.travis/docker-test.sh - after_script: - - docker stop COQ + # - dist: bionic + # language: minimal + # services: + # - docker + # env: + # - COQ=8.11 ELPI="install ${ELPI_811}" CMD="opam pin add coq-hierarchy-builder ." + # install: + # - ./.travis/docker-install.sh + # script: + # - ./.travis/docker-test.sh + # after_script: + # - docker stop COQ - - if: branch = coq-master - dist: bionic - language: minimal - services: - - docker - env: - - COQ=dev ELPI="pin add coq-elpi ${ELPI_DEV}" CMD="opam pin add coq-hierarchy-builder ." - install: - - ./.travis/docker-install.sh - script: - - ./.travis/docker-test.sh - after_script: - - docker stop COQ + # - if: branch = coq-master + # dist: bionic + # language: minimal + # services: + # - docker + # env: + # - COQ=dev ELPI="pin add coq-elpi ${ELPI_DEV}" CMD="opam pin add coq-hierarchy-builder ." + # install: + # - ./.travis/docker-install.sh + # script: + # - ./.travis/docker-test.sh + # after_script: + # - docker stop COQ From 59aec98ea38b5171693c8cf53fda69992210cd09 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 19 May 2020 15:22:37 +0200 Subject: [PATCH 5/8] take into account remanigs in coq-elpi 1.4 --- hb.elpi | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/hb.elpi b/hb.elpi index 9ec4d8e30..a86b9c144 100644 --- a/hb.elpi +++ b/hb.elpi @@ -30,6 +30,8 @@ see phant-abbrev, used to talk about the non canonical name of Foo */ +shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta }. + %%%%%%%%% Elpi Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % This code could be moved in Elpi's standard library @@ -81,7 +83,7 @@ add-abbrev N NParams AbbrevT Global OnlyParse Abbrev :- % runs P in a context where Coq #[attributes] are parsed pred with-attributes i:prop. with-attributes P :- - attributes A, parse-attributes A [att "verbose" bool] Opts, !, + attributes A, coq.parse-attributes A [att "verbose" bool] Opts, !, Opts => P. pred if-verbose i:prop. @@ -1088,8 +1090,7 @@ main-begin-declare Module TName GRFS Decl :- std.do! [ if-verbose (coq.say "HB: postulate type" TName), - coq.univ.new [] U, - Ty = sort (typ U), + coq.fresh-type Ty, coq.env.add-const TName _ Ty tt tt T, % no body, local -> a variable main-declare-context (global (const T)) GRFS _, acc current (clause _ _ (current-decl Decl)) @@ -1167,8 +1168,7 @@ main-begin-declare-builders (context-item IDT _ T none t\ context-item IDF _ (F coq.env.end-module _]) (true), coq.env.begin-section Name, std.assert! (T = sort (typ _)) "The first context item must be a type variable", - coq.univ.new [] U, - Ty = sort (typ U), + coq.fresh-type Ty, coq.env.add-const IDT _ Ty tt tt C, % no body, local -> a variable TheType = global (const C), builders-postulate-factories IDF GRA GRF TheType [], @@ -1226,8 +1226,7 @@ main-declare-asset (asset-parameter Name T Rest as R) D :- std.do! [ if-verbose (coq.say "HB: postulate type" Name), std.assert! (T = sort (typ _)) "The first record parameter must be a type", - coq.univ.new [] U, - Ty = sort (typ U), + coq.fresh-type Ty, coq.env.add-const Name _ Ty tt tt C, % no body, local -> a variable TheType = global (const C), collect-asset-parameters (Rest TheType) [] Module TheType D From d399d644ba7845dd6648e92b81b16f8ba77d597a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 19 May 2020 17:18:48 +0200 Subject: [PATCH 6/8] fix CI wrt release of coq-elpi --- .travis.yml | 99 ++++++++++++++++++++++------------------------------- default.nix | 4 +-- 2 files changed, 42 insertions(+), 61 deletions(-) diff --git a/.travis.yml b/.travis.yml index 12872757b..a2cd4c0e9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -7,17 +7,11 @@ branches: env: global: - CONTRIB_NAME=hb - - ELPI_810=coq-elpi.1.3.0 - - ELPI_811=coq-elpi.1.3.1 + - ELPI_811=coq-elpi.1.4.0 - ELPI_DEV=https://github.com/LPCIC/coq-elpi.git#coq-master jobs: include: - # - language: nix - # env: - # - COQ=8.10 - # script: - # - nix-build --argstr coq-version "${COQ}" - language: nix env: @@ -25,55 +19,42 @@ jobs: script: - nix-build --argstr coq-version "${COQ}" - # - dist: bionic - # language: minimal - # services: - # - docker - # env: - # - COQ=8.10 ELPI="install ${ELPI_810}" CMD="make && make install" - # install: - # - ./.travis/docker-install.sh - # script: - # - ./.travis/docker-test.sh - # after_script: - # - docker stop COQ - - # - dist: bionic - # language: minimal - # services: - # - docker - # env: - # - COQ=8.11 ELPI="install ${ELPI_811}" CMD="make && make install" - # install: - # - ./.travis/docker-install.sh - # script: - # - ./.travis/docker-test.sh - # after_script: - # - docker stop COQ - - # - dist: bionic - # language: minimal - # services: - # - docker - # env: - # - COQ=8.11 ELPI="install ${ELPI_811}" CMD="opam pin add coq-hierarchy-builder ." - # install: - # - ./.travis/docker-install.sh - # script: - # - ./.travis/docker-test.sh - # after_script: - # - docker stop COQ - - # - if: branch = coq-master - # dist: bionic - # language: minimal - # services: - # - docker - # env: - # - COQ=dev ELPI="pin add coq-elpi ${ELPI_DEV}" CMD="opam pin add coq-hierarchy-builder ." - # install: - # - ./.travis/docker-install.sh - # script: - # - ./.travis/docker-test.sh - # after_script: - # - docker stop COQ + - dist: bionic + language: minimal + services: + - docker + env: + - COQ=8.11 ELPI="install ${ELPI_811}" CMD="make && make install" + install: + - ./.travis/docker-install.sh + script: + - ./.travis/docker-test.sh + after_script: + - docker stop COQ + + - dist: bionic + language: minimal + services: + - docker + env: + - COQ=8.11 ELPI="install ${ELPI_811}" CMD="opam pin add coq-hierarchy-builder ." + install: + - ./.travis/docker-install.sh + script: + - ./.travis/docker-test.sh + after_script: + - docker stop COQ + + - if: branch = coq-master + dist: bionic + language: minimal + services: + - docker + env: + - COQ=dev ELPI="pin add coq-elpi ${ELPI_DEV}" CMD="opam pin add coq-hierarchy-builder ." + install: + - ./.travis/docker-install.sh + script: + - ./.travis/docker-test.sh + after_script: + - docker stop COQ diff --git a/default.nix b/default.nix index d7483253c..3056f27a3 100644 --- a/default.nix +++ b/default.nix @@ -16,8 +16,8 @@ let }."${coq-version}"; coq = myCoqPackages.coq; coq-elpi = myCoqPackages.coq-elpi.overrideAttrs(o: { - name = "coq8.11-elpi-784659c"; - src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/784659cbc4ced031b87fc9eda349162169f15084.tar.gz; + name = "coq8.11-elpi-v1.4.0"; + src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/v1.4.0.tar.gz; }); in stdenv.mkDerivation { From 828737a6c6732822a2777388dc38c74c9dd2ea03 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 20 May 2020 15:49:01 +0200 Subject: [PATCH 7/8] merging and shortening default.nix and shell.nix --- default.nix | 57 +++++++++++++++++++++-------------------------------- shell.nix | 36 --------------------------------- 2 files changed, 22 insertions(+), 71 deletions(-) delete mode 100644 shell.nix diff --git a/default.nix b/default.nix index 3056f27a3..2099fe9e3 100644 --- a/default.nix +++ b/default.nix @@ -1,44 +1,31 @@ {withEmacs ? false, nixpkgs ? (fetchTarball { - url = "https://github.com/CohenCyril/nixpkgs/archive/7f59c094a0e5c8659856e611075fe88d6177830f.tar.gz"; - sha256 = "00cf4r8dqfx2hwlwaqb239h72m4s0wl97i98424xd4hki0vzifbi"; + url = "https://github.com/CohenCyril/nixpkgs/archive/8d04d29adb547353ed9fb5c5c4aa6d540e198366.tar.gz"; + sha256 = "1v4l37xkadpnkydpycnk9hrjgh6yc792k66yi7f6203zzr0phzx8"; }), coq-version ? "8.11", print-env ? false }: -with import nixpkgs {}; -let - pgEmacs = emacsWithPackages (epkgs: - with epkgs.melpaStablePackages; [proof-general]); - myCoqPackages = { - "8.10" = coqPackages_8_10; - "8.11" = coqPackages_8_11; - }."${coq-version}"; - coq = myCoqPackages.coq; - coq-elpi = myCoqPackages.coq-elpi.overrideAttrs(o: { - name = "coq8.11-elpi-v1.4.0"; - src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/v1.4.0.tar.gz; - }); -in -stdenv.mkDerivation { +with import nixpkgs { + overlays = [ (super: self: { + coqPackages = { "8.11" = super.coqPackages_8_11; }."${coq-version}"; + coq = self.coqPackages.coq; + })]; +}; +let pgEmacs = emacsWithPackages (epkgs: with epkgs.melpaStablePackages; [proof-general]); in +coqPackages.hierarchy-builder.overrideAttrs (old: { name = "coq${coq.coq-version}-hierarchy-builder-dev"; - src = ./.; - - nativeBuildInputs = [ which ]; - buildInputs = [ coq coq.ocaml coq.ocamlPackages.elpi coq-elpi ]; - - installPhase = ''make -f Makefile.coq VFILES=structures.v COQLIB=$out/lib/coq/${coq.coq-version}/ install''; - - meta = { - description = "Coq plugin embedding ELPI."; - maintainers = [ stdenv.lib.maintainers.cohencyril ]; - license = stdenv.lib.licenses.lgpl21; - inherit (coq.meta) platforms; - inherit (src.meta) homepage; - }; - - passthru = { - compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params; - }; + buildInputs = old.buildInputs ++ + (if lib.trivial.inNixShell then lib.optional withEmacs pgEmacs + else []); } +// (if lib.trivial.inNixShell then { + shellHook = '' + nixEnv (){ + echo "Here is your work environement:" + for x in $buildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done + echo "you can pass option '--argstr coq-version \"x.y\"' to nix-shell to change coq versions" + } + '' + lib.optionalString print-env "nixEnv"; +} else {})) diff --git a/shell.nix b/shell.nix deleted file mode 100644 index c33f19e2e..000000000 --- a/shell.nix +++ /dev/null @@ -1,36 +0,0 @@ -{withEmacs ? false, - nixpkgs ? (fetchTarball { - url = "https://github.com/CohenCyril/nixpkgs/archive/7f59c094a0e5c8659856e611075fe88d6177830f.tar.gz"; - sha256 = "00cf4r8dqfx2hwlwaqb239h72m4s0wl97i98424xd4hki0vzifbi"; -}), - coq-version ? "8.11", - print-env ? false -}: -with import nixpkgs {}; -let - pgEmacs = emacsWithPackages (epkgs: - with epkgs.melpaStablePackages; [proof-general]); - myCoqPackages = { - "8.10" = coqPackages_8_10; - "8.11" = coqPackages_8_11; - }."${coq-version}"; - coq = myCoqPackages.coq; - coq-elpi = myCoqPackages.coq-elpi.overrideAttrs (o: { - name = "coq8.11-elpi-784659c"; - src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/784659cbc4ced031b87fc9eda349162169f15084.tar.gz; - }); -in -stdenv.mkDerivation rec { - name = "env"; - env = buildEnv { name = name; paths = buildInputs; }; - buildInputs = [ coq coq.ocaml coq.ocamlPackages.elpi coq-elpi ] - ++ lib.optional withEmacs pgEmacs - ++ [ pythonPackages.pygments ] ; - shellHook = '' - nixEnv (){ - echo "Here is your work environement:" - for x in $buildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done - echo "you can pass option '--argstr coq-version \"x.y\"' to nix-shell to change coq versions" - } - '' + lib.optionalString print-env "nixEnv"; -} From f9368d97ec3dfebceed8894cb4960a1a114b8d91 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 20 May 2020 15:49:01 +0200 Subject: [PATCH 8/8] updating local opam + commenting override example --- coq-hierarchy-builder.opam | 4 ++-- default.nix | 7 ++++++- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam index 209971605..01653f726 100644 --- a/coq-hierarchy-builder.opam +++ b/coq-hierarchy-builder.opam @@ -11,8 +11,8 @@ dev-repo: "git+https://github.com/math-comp/hierarchy-builder" build: [ make ] install: [ make "install" "VFILES=structures.v" ] depends: [ - "coq" {>= "8.10.0" & < "8.12.0~" } - "coq-elpi" {>= "1.3.0" & < "1.4.0~"} + "coq" {>= "8.11.0" & < "8.12.0~" } + "coq-elpi" {>= "1.4.0" & < "1.5.0~"} ] synopsis: "Hierarchy Builder" description: """ diff --git a/default.nix b/default.nix index 2099fe9e3..691b84b34 100644 --- a/default.nix +++ b/default.nix @@ -8,7 +8,12 @@ }: with import nixpkgs { overlays = [ (super: self: { - coqPackages = { "8.11" = super.coqPackages_8_11; }."${coq-version}"; + coqPackages = { "8.11" = super.coqPackages_8_11; }."${coq-version}".overrideScope' (self: super: { + ## Coq package override example: + # coq-elpi = super.coq-elpi.overrideAttrs (old: { + # name = "coq8.11-elpi-v1.4.0"; + # src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/v1.4.0.tar.gz; + }); coq = self.coqPackages.coq; })]; };