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

49 commits

Author SHA1 Message Date
Kim Morrison
660eb9975a
chore: restore #4006 (#4038) 2024-04-30 23:06:50 +00:00
Leonardo de Moura
4b88965363
chore: disable #4006 (#4021) 
Mathlib is crashing with #4006. Here is the stacktrace produced by Kim:
```
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x100000000000a)
  * frame #0: 0x00000001066db21c libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 2816
    frame #1: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360
    frame #2: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192
    frame #3: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360
    frame #4: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192
    frame #5: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360
    frame #6: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192
    frame #7: 0x00000001066df288 libleanshared.dylib`lean::ir::interpreter::stub_m(lean_object**) + 556
    frame #8: 0x00000001066d6ee0 libleanshared.dylib`lean_object* lean::ir::interpreter::with_interpreter<lean_object*>(lean::environment const&, lean::options const&, lean::name const&, std::__1::function<lean_object* (lean::ir::interpreter&)> const&) + 320
    frame #9: 0x00000001066dee84 libleanshared.dylib`lean::ir::interpreter::stub_m_aux(lean_object**) + 92
    frame #10: 0x00000001066deafc libleanshared.dylib`lean::ir::interpreter::stub_9_aux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*) + 60
    frame #11: 0x00000001066f52a0 libleanshared.dylib`lean_apply_6 + 1748
    frame #12: 0x00000001055d1ac8 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10___lambda__2 + 156
    frame #13: 0x00000001055d47e8 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10___lambda__2___boxed + 144
    frame #14: 0x00000001066f5bcc libleanshared.dylib`lean_apply_7 + 1348
    frame #15: 0x00000001055ccccc libleanshared.dylib`l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__4 + 528
    frame #16: 0x00000001066f5b6c libleanshared.dylib`lean_apply_7 + 1252
    frame #17: 0x00000001055d1550 libleanshared.dylib`l_Lean_Elab_withLogging___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__6 + 240
    frame #18: 0x00000001055d4cb4 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10 + 940
    frame #19: 0x00000001055d5394 libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___lambda__1 + 60
    frame #20: 0x00000001055d5740 libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___lambda__1___boxed + 148
    frame #21: 0x00000001066f11f4 libleanshared.dylib`lean_apply_1 + 840
    frame #22: 0x0000000103bce27c libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1 + 24
    frame #23: 0x0000000103bce4ec libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed + 20
    frame #24: 0x00000001066f10bc libleanshared.dylib`lean_apply_1 + 528
    frame #25: 0x0000000106644260 libleanshared.dylib`lean_profileit + 128
    frame #26: 0x0000000103bce3e0 libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg + 112
    frame #27: 0x00000001055d564c libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore + 268
    frame #28: 0x00000001055d6264 libleanshared.dylib`l_Lean_Elab_Term_applyAttributes + 52
    frame #29: 0x000000010597b840 libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6___lambda__1 + 740
    frame #30: 0x000000010597daf4 libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6___lambda__1___boxed + 124
    frame #31: 0x00000001066f65d8 libleanshared.dylib`lean_apply_8 + 1252
    frame #32: 0x00000001066f5b6c libleanshared.dylib`lean_apply_7 + 1252
    frame #33: 0x0000000104f587b0 libleanshared.dylib`l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSavedPartialInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__2___rarg___lambda__1 + 344
    frame #34: 0x0000000104f59ec4 libleanshared.dylib`l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSavedPartialInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__2___rarg + 280
    frame #35: 0x0000000104f5af20 libleanshared.dylib`l_Lean_Elab_Command_liftTermElabM___rarg___lambda__1 + 144
    frame #36: 0x00000001066f5ab8 libleanshared.dylib`lean_apply_7 + 1072
    frame #37: 0x0000000105636090 libleanshared.dylib`l_Lean_Elab_Term_TermElabM_run___rarg + 844
    frame #38: 0x0000000104f5b8fc libleanshared.dylib`l_Lean_Elab_Command_liftTermElabM___rarg + 1696
    frame #39: 0x000000010597d67c libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6 + 928
    frame #40: 0x000000010597de60 libleanshared.dylib`l_Lean_Elab_Command_elabAttr + 772
    frame #41: 0x000000010597e838 libleanshared.dylib`l_Lean_Elab_Command_elabAttr___boxed + 20
    frame #42: 0x00000001066f2cd4 libleanshared.dylib`lean_apply_3 + 868
    frame #43: 0x0000000104f385f8 libleanshared.dylib`l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__2 + 396
    frame #44: 0x0000000104f39e48 libleanshared.dylib`l___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing + 484
    frame #45: 0x00000001066f2cf0 libleanshared.dylib`lean_apply_3 + 896
    frame #46: 0x0000000104f341d4 libleanshared.dylib`l_Lean_withTraceNode___at_Lean_Elab_Command_runLinters___spec__11 + 788
    frame #47: 0x00000001066f2d54 libleanshared.dylib`lean_apply_3 + 996
    frame #48: 0x00000001066f2cf0 libleanshared.dylib`lean_apply_3 + 896
    frame #49: 0x0000000104f40e30 libleanshared.dylib`l_Lean_Elab_withLogging___at_Lean_Elab_Command_elabCommand___spec__2 + 104
    frame #50: 0x0000000104f4c51c libleanshared.dylib`l_Lean_Elab_Command_elabCommandTopLevel___lambda__1 + 432
    frame #51: 0x00000001066f10e8 libleanshared.dylib`lean_apply_1 + 572
    frame #52: 0x0000000103bce27c libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1 + 24
    frame #53: 0x0000000103bce4ec libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed + 20
    frame #54: 0x00000001066f10bc libleanshared.dylib`lean_apply_1 + 528
    frame #55: 0x0000000106644260 libleanshared.dylib`lean_profileit + 128
    frame #56: 0x0000000103bce3e0 libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg + 112
    frame #57: 0x0000000104f4fce0 libleanshared.dylib`l_Lean_Elab_Command_elabCommandTopLevel + 1284
    frame #58: 0x00000001057d2f30 libleanshared.dylib`l_Lean_Elab_Frontend_elabCommandAtFrontend + 1384
    frame #59: 0x00000001057d63b8 libleanshared.dylib`l_Lean_Elab_Frontend_processCommand + 1332
    frame #60: 0x00000001057d6e48 libleanshared.dylib`l_Lean_Elab_Frontend_processCommands + 72
    frame #61: 0x00000001057d7248 libleanshared.dylib`l_Lean_Elab_IO_processCommands + 212
    frame #62: 0x00000001057d83d0 libleanshared.dylib`l_Lean_Elab_runFrontend___lambda__3 + 76
    frame #63: 0x00000001057d96d0 libleanshared.dylib`lean_run_frontend + 2436
    frame #64: 0x00000001065e72b4 libleanshared.dylib`lean::run_new_frontend(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>> const&, lean::options const&, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>> const&, lean::name const&, unsigned int, lean::optional<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>>> const&, unsigned char) + 244
    frame #65: 0x00000001065e9c8c libleanshared.dylib`lean_main + 8348
    frame #66: 0x0000000184f93f28 dyld`start + 2236
```

cc @Kha
 2024-04-29 10:58:11 +00:00
Leonardo de Moura
99e8270d2d
fix: proposition fields must be theorems (#4006) 
closes #2575
 2024-04-28 01:59:47 +00:00
Gabriel Ebner
4544443d98 feat: reorder tc subgoals according to out-params 2023-04-10 13:00:04 -07:00
Leonardo de Moura
ffb0f42aae fix: fixes #1901 2022-12-01 08:39:06 -08:00
Leonardo de Moura
081dff288f fix: debug build 2022-04-13 13:12:53 -07:00
Leonardo de Moura
efb859013e chore: ignore {} annotations at mk_projections 2022-04-13 10:16:41 -07:00
Leonardo de Moura
1afee372f7 refactor: move consume_type_annotations declaration to expr.h 2022-03-10 08:00:39 -08:00
Leonardo de Moura
33883e9d2a fix: resulting type of projection functions should not include auxiliary type annotations (e.g., autoParam) 2022-03-10 07:47:38 -08:00
Sebastian Ullrich
b13d3e6ca5 fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
Leonardo de Moura
c8406a301d chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
Leonardo de Moura
b575087859 fix: unfold class projections when using TransparencyMode.instances 2021-01-25 12:30:26 -08:00
Leonardo de Moura
8c2cb44ac0 fix: error message produced by lean_mk_projections 2020-12-22 17:40:32 -08:00
Leonardo de Moura
de568b1268 chore: remove dead code 2020-10-28 09:33:19 -07:00
Leonardo de Moura
f36f7592e6 chore: move to new frontend 2020-10-15 16:18:42 -07:00
Leonardo de Moura
7f43d01703 fix: assertion violation 2020-07-24 14:54:20 -07:00
Leonardo de Moura
ca2e82f39b feat: add projections 2020-07-23 16:42:34 -07:00
Leonardo de Moura
7c76a19885 chore: fix includes 2020-05-22 14:17:25 -07:00
Leonardo de Moura
8bdca35282 chore: use #include <lean/runtime/...> for runtime .h files 2020-05-18 11:30:07 -07:00
Leonardo de Moura
a124461dca chore: rename projection function major field to self 
This is useful for projection function for classes + named arguments.
 2019-12-12 08:55:55 -08:00
Leonardo de Moura
4a6d0a8082 feat: projections of classes should not be reducible 2019-11-23 09:25:49 -08: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
0888dee25e chore(*): meta ==> unsafe 2019-03-15 15:04:40 -07:00
Leonardo de Moura
c3569dc72d feat(kernel): store structure name in proj-expressions 2018-10-02 09:23:11 -07:00
Leonardo de Moura
fabfe32ca5 chore(*): remove unnecessary scoped_ext dependencies 2018-09-08 15:42:48 -07:00
Leonardo de Moura
58e91559d0 feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
Leonardo de Moura
8ed89c6ac3 chore(library): remove normalize.cpp 
The command `#reduce` was also temporarily removed.
 2018-09-04 10:51:14 -07:00
Leonardo de Moura
dd03747d22 chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies 2018-09-03 13:05:42 -07:00
Leonardo de Moura
82095cc018 refactor(kernel): split declaration into declaration and constant_info 
This is just another step towards the design described at commit 16598391a07d4a
 2018-08-22 17:53:11 -07:00
Leonardo de Moura
f3e99286bb chore(kernel): remove certified_declaration 2018-08-22 12:11:34 -07:00
Leonardo de Moura
fd5bfc7dfe refactor(kernel): simplify binder_info 
Now, it is an enumeration type like its Lean counterpart.
 2018-06-20 15:31:40 -07:00
Leonardo de Moura
eee4e00364 feat(library/constructions/projection): implement projections using expr.proj constructor 2018-06-19 17:26:31 -07:00
Leonardo de Moura
8ae1e51b6d feat(kernel): distinguish kernel_exceptions using different classes 2018-06-07 16:28:54 -07:00
Leonardo de Moura
c0e1d05199 chore(kernel): type_checker ==> old_type_checker 2018-06-06 16:10:40 -07:00
Leonardo de Moura
3c1ccc9b74 refactor(kernel): use m_meta instead of m_trusted 2018-05-31 11:18:00 -07:00
Leonardo de Moura
0556412f8d refactor(*): add runtime folder 
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
 2018-05-14 14:23:56 -07:00
Sebastian Ullrich
1abf8738fc feat(frontends/lean/structure_cmd): allow implicitness infer annotation and parameters in field declaration 2018-02-28 12:49:22 +01:00
Leonardo de Moura
21e52408b2 refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name 2018-02-21 15:04:19 -08:00
Sebastian Ullrich
dc5e50e7f0 feat(frontends/lean/structure_cmd): hide out_param in projections 2018-02-02 08:58:52 -08:00
Sebastian Ullrich
3f497b8d8e fix(library/constructions/projection): out_params should always be implicit in projections 2018-02-02 08:58:52 -08:00
Gabriel Ebner
9920062b69 fix(kernel/expr,library/constructions/projection): preserve instance-implicitness in structure parameters 2017-08-27 16:47:04 +02:00
Gabriel Ebner
776b440d55 fix(library/constructions/projection): fix macro expansion 
Thanks to @fpvandoorn for noticing this issue in Lean 2!  We encountered
this situation when the inferred type of the projection argument did not
reduce to the structure type with the current transparency setting of
the type context.
 2017-07-18 19:56:20 +01:00
Sebastian Ullrich
491802409a chore(*): remove unused macro_definition_cell::pp method 2017-05-24 09:51:23 +02:00
Sebastian Ullrich
e9a6c544af refactor(frontends/lean/{elaborator,structure_cmd}): compile structure inheritance to nested fields 2017-04-24 19:35:15 +02:00
Leonardo de Moura
d0d75c0923 refactor(kernel): reduce number of configurations supported in the kernel 
Now, eta and impredicativity are assumed to be always true.

Motivation: the rest of the system assumes eta.
Regarding impredicativity, we decided to support only the standard library.
 2016-09-27 17:07:01 -07:00
Leonardo de Moura
932d14241b chore(kernel): remove support for mutually inductive datatypes from the kernel 2016-09-10 17:39:17 -07:00
Leonardo de Moura
81a30a69d2 refactor(library/normalize): remove unfold and unfold_full attributes 2016-09-05 08:40:58 -07:00
Leonardo de Moura
f7df7dc9a7 refactor(kernel): add reducibility_hints 2016-09-04 16:30:02 -07:00
Leonardo de Moura
f056f0f2cb refactor(library): definitional ==> constructions 2016-08-11 10:08:22 -07:00
Renamed from src/library/definitional/projection.cpp (Browse further)