[Merged by Bors] - chore: cleanup for mathport update #620
Conversation
|
bors merge |
* `add_decl_doc` already exists in core (this declaration was just shadowing it) * `setup_tactic_parser` is not planned for porting; the nearest equivalent is nothing at all * `mk_simp_attribute` can mostly be aligned to `register_simp_attr`, and the remaining part (the `:= ids,*`) can't be supported at all and will give a suitable port message in mathport * `std_next` alignment consistently gives a stack overflow when porting on my machine; I think this is a recent regression (possibly leanprover-community/mathport#192?) but this is a quick fix since this function doesn't matter too much.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
I don't think this is related to 192. That issue is about binported type class instances that break Lean 4. Those typically don't cause stack overflows. |
|
Just to clarify, the issue that happens is that when synport is translating a theorem (the binport part, which translates the environment), it first tries to use the given definition, then stubs the value and then the type if it hits defeq issues. The problem is that even though it is in a try catch, the first attempt fails with an uncatchable stack overflow due to things being almost defeq but with a bunch of lets and a bunch of big numerals it seems like something is blowing up in the term. |
add_decl_docalready exists in core (this declaration was just shadowing it)setup_tactic_parseris not planned for porting; the nearest equivalent is nothing at allmk_simp_attributecan mostly be aligned toregister_simp_attr, and the remaining part (the:= ids,*) can't be supported at all and will give a suitable port message in mathportstd_nextalignment consistently gives a stack overflow when porting on my machine; I think this is a recent regression (possibly Notations no longer work in binport mathport#192?) but this is a quick fix since this function doesn't matter too much.