From 5215ed6b216fedb37bfd241666048d9a4126b2b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Fri, 4 Aug 2017 19:46:16 +0200 Subject: [PATCH 1/4] compcert: fix breakage on linux after f130ecd --- pkgs/top-level/all-packages.nix | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index eb59deba7e82..9f72b84f1825 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -5221,13 +5221,9 @@ with pkgs; cmucl_binary = callPackage_i686 ../development/compilers/cmucl/binary.nix { }; - compcert = callPackage ../development/compilers/compcert (( - if system == "x86_64-linux" - then { tools = pkgsi686Linux.stdenv.cc; } - else {} - ) // { + compcert = callPackage ../development/compilers/compcert { coq = coq_8_6; - }); + }; # Users installing via `nix-env` will likely be using the REPL, From c0dca2fb00a4e94f995b2752c78f4e67a6c6e7c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Fri, 4 Aug 2017 19:46:16 +0200 Subject: [PATCH 2/4] coq: 8.6 -> 8.6.1 --- pkgs/applications/science/logic/coq/default.nix | 3 ++- pkgs/top-level/all-packages.nix | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index f93856e90e11..284175d2b4c7 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -9,7 +9,7 @@ , ocamlPackages, ncurses , buildIde ? true , csdp ? null -, version ? "8.6" +, version ? "8.6.1" }: let @@ -18,6 +18,7 @@ let "8.5pl2" = "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3"; "8.5pl3" = "0fyk2a4fpifibq8y8jhx1891k55qnsnlygglch64sva0bph94nrh"; "8.6" = "1pw1xvy1657l1k69wrb911iqqflzhhp8wwsjvihbgc72r3skqg3f"; + "8.6.1" = "17cg2c40y9lskkiqfhngavp8yw3shpqgkpihh30xx0rlhn9amy1j"; }."${version}"; coq-version = builtins.substring 0 3 version; camlp5 = ocamlPackages.camlp5_transitional; diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 9f72b84f1825..d93baafaa8f7 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -5222,7 +5222,8 @@ with pkgs; cmucl_binary = callPackage_i686 ../development/compilers/cmucl/binary.nix { }; compcert = callPackage ../development/compilers/compcert { - coq = coq_8_6; + # Pin the version of coq used in compcert to 8.6 until the next release + coq = callPackage ../applications/science/logic/coq { version = "8.6"; }; }; From b25d65e0513b59a7767ca627ab61ed84c3ea0768 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Fri, 4 Aug 2017 19:46:16 +0200 Subject: [PATCH 3/4] coq: use camlp5_strict The versions of Coq available through this expression do not actually require camlp5_transitional. We drop this dependency to see if, in the future, the package camlp5_transitional can be removed from nixpkgs. --- pkgs/applications/science/logic/coq/default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 284175d2b4c7..3f4be58c2667 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -21,7 +21,7 @@ let "8.6.1" = "17cg2c40y9lskkiqfhngavp8yw3shpqgkpihh30xx0rlhn9amy1j"; }."${version}"; coq-version = builtins.substring 0 3 version; - camlp5 = ocamlPackages.camlp5_transitional; + camlp5 = ocamlPackages.camlp5_strict; ideFlags = if buildIde then "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; csdpPatch = if csdp != null then '' substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp" From 057ffcf0ddb3f94b8cc6899b6d5bfe7f93f1014e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Fri, 4 Aug 2017 19:46:16 +0200 Subject: [PATCH 4/4] coq: adding myself to the maintainers --- lib/maintainers.nix | 1 + pkgs/applications/science/logic/coq/default.nix | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/lib/maintainers.nix b/lib/maintainers.nix index 17629daea479..c0a8f3f32319 100644 --- a/lib/maintainers.nix +++ b/lib/maintainers.nix @@ -632,6 +632,7 @@ zauberpony = "Elmar Athmer "; zef = "Zef Hemel "; zimbatm = "zimbatm "; + Zimmi48 = "Théo Zimmermann "; zohl = "Al Zohali "; zoomulator = "Kim Simmons "; zraexy = "David Mell "; diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 3f4be58c2667..9620140dde4b 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -133,7 +133,7 @@ self = stdenv.mkDerivation { homepage = http://coq.inria.fr; license = licenses.lgpl21; branch = coq-version; - maintainers = with maintainers; [ roconnor thoughtpolice vbgl ]; + maintainers = with maintainers; [ roconnor thoughtpolice vbgl Zimmi48 ]; platforms = platforms.unix; }; }; in self