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

10856 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
941bbd3e96 fix(library/tactic/congruence/congruence_closure): crash when processing partially applied constructors 2016-12-26 18:51:03 -08:00
Leonardo de Moura
7a2ae8d40b test(tests/lean/run/ematch1): add ematching example 2016-12-26 18:26:57 -08:00
Leonardo de Moura
15f1c6bab2 chore(library/tactic/congruence/ematch): style 2016-12-26 18:23:57 -08:00
Leonardo de Moura
f3f1ec268b chore(library/init/meta/tactic): make all arguments in id_locked explicit. 2016-12-26 18:22:37 -08:00
Leonardo de Moura
6661faf3da fix(library/tactic/congruence/congruence_closure): but at add_occurrence 2016-12-26 18:13:06 -08:00
Leonardo de Moura
8419219ca6 feat(library/tactic/congruence/congruence_closure): add trace.debug.cc option 2016-12-26 18:13:02 -08:00
Leonardo de Moura
148d34b3bf feat(library/tactic/congruence/congruence_closure): merge annotated term with term being annotated 2016-12-26 16:30:18 -08:00
Leonardo de Moura
cf32e25f68 fix(frontends/lean/pp): pretty print pattern hints 2016-12-26 16:13:41 -08:00
Leonardo de Moura
9e46818563 feat(library/tactic/congruence): ematching 2016-12-26 15:52:18 -08:00
Leonardo de Moura
6a5f6a84cd feat(library/tactic/congruence/hinst_lemma): add heuristic instantiation lemmas 2016-12-25 20:11:58 -08:00
Leonardo de Moura
7d1c48e673 fix(frontends/lean/definition_cmds): "elaboration time" for lemmas was not being reported when using profiler 2016-12-25 16:49:58 -08:00
Leonardo de Moura
61d007892b feat(library/data/stream): add stream module 2016-12-25 16:40:52 -08:00
Leonardo de Moura
9b35adfc8c feat(library/tactic/congruence/congruence_closure): add support for constructor equalities 2016-12-25 12:47:17 -08:00
Leonardo de Moura
7f4160bb4b feat(library/constructions): add helper procedures for building injection and inconsistency proofs for constructor equalities 2016-12-25 12:44:33 -08:00
Leonardo de Moura
a30081a715 feat(library/tactic/congruence/congruence_closure): interpreted values in the same equivalence class 2016-12-25 11:09:55 -08:00
Leonardo de Moura
b6051a6a03 feat(library/init/meta/congruence_tactics): add cc_dbg that display equivalence classes at failure 2016-12-25 10:46:15 -08:00
Leonardo de Moura
b313328cb9 feat(library/equations_compiler): int constants 2016-12-25 10:00:18 -08:00
Leonardo de Moura
f9fb041e04 fix(library/comp_val): mk_int_val_ne_proof 
There was a typo in the proof generation. The weird part is that the
proof was valid, but it was very inefficient to check.
The proof was valid because ((n:int) ≥ m) reduces to true/false if n and
m are integer numerals. Thus, if ((n:int) ≥ m) holds then `trivial` is a
valid proof.
However, the reduction is extremely inefficient since it relies on
computations in unary.

In the buggy version, we provided a proof for (a >= 0) where (b >= 0)
was expected. However, both types are definitionally equal to true.
This is why the proof worked.
 2016-12-24 15:54:48 -08:00
Leonardo de Moura
3061d8b9a3 feat(library): add mk_int_val_ne_proof 2016-12-24 15:22:31 -08:00
Leonardo de Moura
58ca9a3059 feat(library/init/data/int/comp_lemmas): add auxiliary lemmas for comparing int numerals 2016-12-24 13:52:48 -08:00
Leonardo de Moura
8f401c8752 chore(library/tactic/congruence/congruence_closure): remove unnecessary field 2016-12-24 09:14:25 -08:00
Leonardo de Moura
0906d84c92 fix(library/tactic/congruence/congruence_closure): proof generation for congruence with different arity 2016-12-24 09:12:10 -08:00
Leonardo de Moura
a3600b6f98 test(tests/lean/run/cc6): add more cc tests 2016-12-24 08:50:51 -08:00
Leonardo de Moura
424a6acb68 fix(library/tactic/congruence/congruence_closure): missing proof construction step 2016-12-24 08:43:04 -08:00
Leonardo de Moura
a176bd324d fix(library/tactic/congruence/congruence_closure): check_eq_true 2016-12-23 22:24:39 -08:00
Leonardo de Moura
a13d3c83c9 fix(library/tactic/congruence/congruence_closure): heq bug and add more tests 2016-12-23 21:57:49 -08:00
Leonardo de Moura
b1b694a532 fix(library/tactic/congruence/congruence_closure): bugs, and add basic cc tactic 2016-12-23 19:30:45 -08:00
Leonardo de Moura
ca261b7fa8 feat(library/init/meta/congruence_tactics): add option for retrieving only non-singleton equivalence classes, add auxiliary functions 2016-12-23 18:35:44 -08:00
Leonardo de Moura
a2850ac050 fix(library/tactic/congruence/congruence_closure): bugs in the fo-approx mode, and debug mode compilation errors 2016-12-23 17:31:20 -08:00
Leonardo de Moura
1aa92c7d7d fix(library/tactic/congruence/congruence_closure): add entries for 'true' and 'false' 2016-12-23 15:54:09 -08:00
Leonardo de Moura
d431d7274a feat(library/tactic/congruence/congruence_closure): hard code support for ne 2016-12-23 15:37:05 -08:00
Leonardo de Moura
6eb81d2472 feat(library/tactic/congruence/congruence_closure): add new configuration options for minimizing the number of entries and occurrences 2016-12-23 15:18:10 -08:00
Daniel Selsam
95882c14cd feat(init/data/string/basic.lean): inhabited string 2016-12-23 14:45:53 -08:00
Leonardo de Moura
a4173467c4 feat(library/app_builder): use Semireducible if caller did not specify a transparency_mode and ctx.mode() is Reducible or None 
see discussion at #1265
 2016-12-23 14:41:22 -08:00
Leonardo de Moura
17cc40b35e feat(library/tactic/congruence/congruence_closure): do not recurse on values and instances when internalizing terms 2016-12-23 13:24:43 -08:00
Leonardo de Moura
9209947d4a chore(CMakeLists): uncomment tcmalloc configuration 2016-12-23 11:57:50 -08:00
Leonardo de Moura
b3ef489b9a chore(doc/make/cygwin): we do not support cygwin anymore (only MSYS2) 2016-12-23 10:01:08 -08:00
Leonardo de Moura
61c9fdd908 chore(doc/lean): remove unnecessary files 2016-12-23 10:00:30 -08:00
Leonardo de Moura
8027e3c0e2 chore(doc/lean): remove old documentation 2016-12-23 09:58:45 -08:00
Leonardo de Moura
237f331569 chore(README): remove link to short tutorial 2016-12-23 09:49:52 -08:00
Leonardo de Moura
461cc0d015 fix(tests/lean/test_single): remove .tmp files, avoid -i option 2016-12-23 09:48:02 -08:00
Gabriel Ebner
d079f66017 fix(tests/lean/test_single): work around sed on mac 2016-12-23 17:49:20 +01:00
Gabriel Ebner
1e827c1e20 fix(tests/lean/test_single): fix missing_import test on windows 2016-12-23 11:24:45 +01:00
Gabriel Ebner
15157bdf0b feat(frontends/lean/parser): keep going after failed imports 2016-12-23 10:53:47 +01:00
Gabriel Ebner
e3b3de5cf3 fix(module_mgr): guard all accesses to m_mod_info 2016-12-23 18:01:44 +01:00
Leonardo de Moura
104ee1b120 fix(library/tactic/congruence/congruence_tactics): stupid mistake 2016-12-22 20:54:20 -08:00
Leonardo de Moura
6329afc121 chore(library/tactic/congruence/congruence_closure): fix typo 2016-12-22 20:05:02 -08:00
Leonardo de Moura
77737a621d fix(library/tactic/congruence/congruence_closure): name collision, we had congr_lemma_cache in two different modules 2016-12-22 19:35:38 -08:00
Leonardo de Moura
94e6fbcbbf perf(library/vm/vm): make sure builtin cases_on recursors are assigned ids first 
This will minimize the size of the m_builtin_cases_vector.
It also indirectly prevents the crash decribed at 144d9096e2.
However, the fix used there is more robust.
 2016-12-22 18:46:51 -08:00
Leonardo de Moura
144d9096e2 fix(library/vm/vm): serialization/deserialization of builtin cases_on instruction 
We generate internal ids for builtin cases_on recursors.
These ids were being saved in the .olean files.
This was fine before commit 41e8a1712e because we had a separate
mapping for builtin cases_on recursors. Now, all ids are stored in the
same mapping. Thus, minor changes in the set of VM builtin operations
make lean crash when importing .olean files because they will change the
internal id for the builtin cases_on.
The problem can be reproduced in the following way:

0- Go to build/release

1- make clean-olean

2- make
Everything is fine after step 2

3- Comment the following line at tactic_state.cpp

    DECLARE_VM_BUILTIN(name({"tactic", "open_namespaces"}),      tactic_open_namespaces);

4- make

5- Lean will crash when executing the following command

   ../../bin/lean ../../library/init/meta/tactic.lean

I believe this bug is reponsible by the crash that @jroesch reported on Slack.

This commit fixes the problem by storing the name of the builtin
cases_on recursor in the .olean file.
 2016-12-22 18:35:30 -08:00