max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
16508 commits 1 branch 0 tags 5.3 GiB
Commit graph

16508 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
9a3a01fa6e feat(library/compiler/compiler): invoke new IR compiler implemented in Lean 2019-05-16 16:08:52 -07:00
Leonardo de Moura
9d7191feca chore(library/compiler): remove support for fully boxed 2019-05-16 15:48:33 -07:00
Leonardo de Moura
ac69f802e1 feat(library/compiler): interface with new IR compiler entry point 2019-05-16 15:41:47 -07:00
Leonardo de Moura
aa138fe686 chore(*): get_obj_arg => to_obj_arg 2019-05-16 14:42:02 -07:00
Leonardo de Moura
9d9f546ad8 refactor(util/sexpr): move options and option_declarations to util 2019-05-16 14:37:24 -07:00
Leonardo de Moura
367b3ec4a3 chore(tests/util): remove old test 2019-05-16 14:29:26 -07:00
Leonardo de Moura
9c4da289b2 refactor(util/sexpr/options): options as a Lean object 2019-05-16 14:27:44 -07:00
Leonardo de Moura
31d4fa9f71 chore(util/sexpr/options): shrink options API 
Motivation: move to the Lean implementation
 2019-05-16 14:08:11 -07:00
Leonardo de Moura
5482a11642 feat(library/init/lean/compiler/ir/default): add new entry point 2019-05-16 10:20:00 -07:00
Leonardo de Moura
2d065c7ded feat(library/init/lean/compiler/ir): add Lean.IR.CompilerM 
and environment extension for storing Lean IR declarations.
 2019-05-16 10:20:00 -07:00
Sebastian Ullrich
7a19f246e6 fix(shell/lean): re-add missing short-only option 2019-05-16 10:27:18 +02:00
Leonardo de Moura
739008f8d4 chore(library/init/lean/compiler/llnf): disable 
I am going to refactor the interface with the new IR compiler.
 2019-05-15 19:02:51 -07:00
Leonardo de Moura
77768c504e feat(shell/lean): import time stats 2019-05-15 17:16:19 -07:00
Leonardo de Moura
9b3421b63b feat(library/compiler/closed_term_cache): remove C++ implementation and use Lean one 2019-05-15 15:33:46 -07:00
Leonardo de Moura
b87afdcbfd chore(library/init/lean/compiler/closedtermcache): naming convention 2019-05-15 15:19:09 -07:00
Leonardo de Moura
816e83970b refactor(util/object_ref, kernel/environment): move to_optional 2019-05-15 15:16:29 -07:00
Leonardo de Moura
09df708af2 feat(library/init/lean/compiler): implement close term cache env extension in Lean 2019-05-15 11:01:25 -07:00
Leonardo de Moura
7212fbab6e perf(library/init/lean/environment): search hashmap first 
Hypothesis: the vast majority of Environment queries try to access
imported constants instead of local ones.
 2019-05-15 11:01:25 -07:00
Leonardo de Moura
70dce4b775 feat(library/init/lean/environment): show rbmap depth and hashmap bucket size 2019-05-15 11:01:25 -07:00
Leonardo de Moura
89e01368cd fix(library/init/lean/environment): throw error if environment already contains constant 2019-05-15 11:01:25 -07:00
Leonardo de Moura
3193e91aff feat(library/init/lean/environment): add Environment.displayStats and --stats command line argument 2019-05-15 11:01:25 -07:00
Leonardo de Moura
bc809643ec feat(library/init/lean/expr): add Expr.quickLt, Expr.eqv 2019-05-15 11:01:25 -07:00
Sebastian Ullrich
f78c4a901f feat(tests/playground/report): cache misses via perf stat 2019-05-15 19:39:55 +02:00
Sebastian Ullrich
9cdcb99008 fix(tests/playground/Makefile): fixes 2019-05-15 17:57:25 +02:00
Sebastian Ullrich
a831ce85d7 feat(tests/playground/report): fixed output format 2019-05-15 17:35:03 +02:00
Sebastian Ullrich
20dde07316 feat(tests/playground/report): %GC times 2019-05-15 17:35:00 +02:00
Sebastian Ullrich
e0b45d65f7 feat(default.nix,tests/playground): Nix-powered benchmark suite 2019-05-15 13:25:29 +02:00
Leonardo de Moura
8ab15536a7 perf(library/init/data/array/binsearch): add binSearchContains 2019-05-14 20:52:57 -07:00
Leonardo de Moura
45eda6d81b perf(library/init/lean/modifiers): add only local entries to state 
We can use `getModuleEntries` and `getModuleIdxFor` to test whether a
constant is protected or not.
 2019-05-14 20:30:46 -07:00
Leonardo de Moura
dc71fafac1 feat(library/init/data/array): add Array.binSearch 2019-05-14 18:25:54 -07:00
Leonardo de Moura
2e4f5951e3 feat(library/init/data/array/qsort): simple quicksort 
@kha I added `qsort` for sorting environment extension entries, but I am
wondering if we could use it as a benchmark in our paper. It is a pure implementation; it is
fast; it implements the real quick sort algorithm with in-place updates if the
input array is not shared. If the array is shared it performs
a single copy and then switches to in-place updates.
 2019-05-14 17:46:34 -07:00
Leonardo de Moura
431c0a2525 chore(stage0): update 2019-05-14 16:28:25 -07:00
Leonardo de Moura
5fa924ff4a feat(library/init/lean/environment): improve registerPersistentEnvExtension signature 2019-05-14 16:25:43 -07:00
Leonardo de Moura
c957450d05 feat(library/protected): replace C++ implementation with Lean one 2019-05-14 16:12:56 -07:00
Leonardo de Moura
da5b900cbd feat(library/init/lean): add protected extension 2019-05-14 16:04:24 -07:00
Leonardo de Moura
3a3da7dfdf chore(library/init/env_ext): update 2019-05-14 15:45:10 -07:00
Leonardo de Moura
b888b6f3b6 feat(library/init/lean/environment): process imported entries 2019-05-14 15:32:07 -07:00
Leonardo de Moura
59235c1899 chore(library/init/lean/environment): ModuleId ==> ModuleIdx 2019-05-14 13:02:43 -07:00
Leonardo de Moura
5e2111f4a4 fix(library/init/lean/environment): process entries using the order they were inserted 2019-05-14 12:53:50 -07:00
Leonardo de Moura
a24a1562ea fix(library/init/lean/environment): import order 2019-05-14 12:41:19 -07:00
Leonardo de Moura
5df0b05cc7 chore(library/init/lean/environment): remove get_modifications_core 2019-05-14 11:26:04 -07:00
Leonardo de Moura
edeae776da chore(library/module): module::add for declarations is not needed anymore 2019-05-14 11:23:35 -07:00
Leonardo de Moura
7696c28fe1 feat(library/module): module manager in Lean is alive 2019-05-14 11:10:49 -07:00
Leonardo de Moura
d5fd5d86ee fix(library/init/lean/environment): quotInit initialization 2019-05-14 10:31:06 -07:00
Leonardo de Moura
02e558d781 feat(library/init/lean/environment): export module I/O in Lean 2019-05-14 10:15:33 -07:00
Leonardo de Moura
642c4c59bd feat(library/init/lean/environment): support for serializing/performing legacy modification objects 2019-05-14 10:08:31 -07:00
Leonardo de Moura
dbb519d826 feat(library/init/lean/environment): importModules draft 2019-05-14 08:58:29 -07:00
Leonardo de Moura
67d14705b0 chore(library/module): simplify write_module 2019-05-14 08:08:09 -07:00
Leonardo de Moura
427852d759 feat(library/init/lean/environment): add findOLean 2019-05-14 08:02:26 -07:00
Leonardo de Moura
e616def866 chore(library/module): remove dead declaration 2019-05-14 07:53:44 -07:00