max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update cross benches

Browse source
This commit is contained in:
Sebastian Ullrich 2020-08-18 11:44:29 +02:00
parent d059d28c22
commit 5e48d2bb7d
3 changed files with 23 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
tests/bench/cross.nix
View file

@ -2,20 +2,20 @@
let
# pin Lean commit to avoid rebuilds
# 2020-03-04
lean = import (builtins.fetchGit { url = ../../.; rev = "21ca3709612ff7a05f0e5aa0849d776c1bc6d751"; }) {};
# 2020-08-18
lean = import (builtins.fetchGit { url = ../../.; rev = "d059d28c220247d51310c4ea437807c3446d36d7"; }) {};
# for binarytrees.hs
ghcPackages = p: [ p.parallel ];
ghc = pkgs.haskell.packages.ghc883.ghcWithPackages ghcPackages; #.override { withLLVM = true; };
ocaml = pkgs.ocaml-ng.ocamlPackages_latest.ocaml;
ghc = pkgs.haskell.packages.ghc884.ghcWithPackages ghcPackages; #.override { withLLVM = true; };
ocaml = pkgs.ocaml-ng.ocamlPackages_4_11.ocaml;
# note that this will need to be compiled from source
ocamlFlambda = ocaml.override { flambdaSupport = true; };
mlton = pkgs.mlton;
mlkit = pkgs.stdenv.mkDerivation {
name = "mlkit";
src = pkgs.fetchzip {
url = "https://github.com/melsman/mlkit/releases/download/mlkit-4.4.2/mlkit_bin_dist.tgz";
sha256 = "079299h5m3gkk10qpn2r6va7kjj0sr9z3cs0knjz3qv1cldpzj7x";
src = builtins.fetchTarball {
url = "https://github.com/melsman/mlkit/releases/download/v4.5.0/mlkit_bin_dist.tgz";
sha256 = "1nrk2klhrr2xcm83y601w6dffl756qfk4kgvn3rkjlp7b2i8r8mr";
};
buildInputs = [ pkgs.makeWrapper ];
dontBuild = true;
@ -29,7 +29,7 @@ let
'';
};
swift = pkgs.swift;
temci = import (builtins.fetchGit { url = http://github.com/parttimenerd/temci.git; rev = "ba1505a7c2de471a5821a2643b34de2d1c1af03e"; }) {};
temci = import (builtins.fetchGit { url = http://github.com/parttimenerd/temci.git; rev = "743a6ee9328fc8cb85d334dbce23a89d14cef4c5"; }) {};
in pkgs.stdenv.mkDerivation rec {
name = "bench";
src = pkgs.lib.sourceFilesBySuffices ./. ["Makefile" "leanpkg.path" "temci.yaml" ".py" ".lean" ".hs" ".ml" ".sml"];
@ -37,17 +37,17 @@ in pkgs.stdenv.mkDerivation rec {
#LEAN_GCC_BIN = "${lean { stdenv = pkgs.gcc9Stdenv; }}/bin";
LEAN_NO_REUSE_BIN = "${lean.overrideAttrs (attrs: {
prePatch = ''
substituteInPlace src/Init/Lean/Compiler/IR.lean --replace "decls.map Decl.insertResetReuse" "decls"
substituteInPlace src/shell/CMakeLists.txt --replace "install(TARGETS lean DESTINATION bin)" "install(PROGRAMS $<TARGET_FILE:lean_stage2> DESTINATION bin RENAME lean)"
substituteInPlace src/Lean/Compiler/IR.lean --replace "decls.map Decl.insertResetReuse" "decls"
'';
buildFlags = [ "lean_stage2" ];
buildFlags = [ "stage1.5" ];
installFlags = [ "-C stage1.5" ];
})}/bin";
LEAN_NO_BORROW_BIN = "${lean.overrideAttrs (attrs: {
prePatch = ''
substituteInPlace src/Init/Lean/Compiler/IR.lean --replace "inferBorrow" "pure"
substituteInPlace src/shell/CMakeLists.txt --replace "install(TARGETS lean DESTINATION bin)" "install(PROGRAMS $<TARGET_FILE:lean_stage2> DESTINATION bin RENAME lean)"
substituteInPlace src/Lean/Compiler/IR.lean --replace "inferBorrow" "pure"
'';
buildFlags = [ "lean_stage2" ];
buildFlags = [ "stage1.5" ];
installFlags = [ "-C stage1.5" ];
})}/bin";
LEAN_NO_ST_BIN = "${lean.overrideAttrs (attrs: { patches = [ ./disable-st.patch ]; })}/bin";
PARSER_TEST_FILE = lean.src + "/src/Init/Core.lean";

8
tests/bench/disable-st.patch
View file

@ -4,13 +4,13 @@ Date: Mon, 11 Nov 2019 18:15:21 +0100
Subject: [PATCH] disable ST objects
---
src/runtime/lean.h | 6 +++---
src/include/lean/lean.h | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/runtime/lean.h b/src/runtime/lean.h
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 6b37fd91a..c53137860 100644
--- a/src/runtime/lean.h
+++ b/src/runtime/lean.h
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -567,13 +567,13 @@ void lean_mark_persistent(lean_object * o);
static inline void lean_set_st_header(lean_object * o, unsigned tag, unsigned other) {

8
tests/bench/nixpkgs.nix
View file

@ -1,5 +1,7 @@
import (builtins.fetchTarball {
name = "nixpkgs-unstable-2020-03-04";
url = https://github.com/NixOS/nixpkgs/archive/d881de1e9641735ef3fd6beffb1a6006140baf17.tar.gz;
sha256 = "0mwgzjk0h7r7hv6mmaq54lw7wicwzp170z228h4j5yi5g2dz63kh";
name = "nixpkgs-unstable-2020-08-18";
# Commit hash from `git ls-remote https://github.com/NixOS/nixpkgs-channels nixpkgs-unstable`
url = https://github.com/nixos/nixpkgs/archive/c5815280e92112a25d958a2ec8b3704d7d90c506.tar.gz;
# Hash obtained using `nix-prefetch-url --unpack <url>`
sha256 = "09ic4s9s7w3lm0gmcxszm5j20cfv4n5lfvhdvgi7jzdbbbdps1nh";
}) {}