feat: test that an executable importing Aesop works

[kim-em]

Currently, any executable importing Aesop will segfault on initialization.

lake test

segfaults under this PR, which adds a minimal executable.

lake env lldb .lake/build/bin/aesop_test_executable 

followed by the lldb commands run and bt shows the stack trace:

% lake env lldb .lake/build/bin/aesop_test_executable                 
(lldb) target create ".lake/build/bin/aesop_test_executable"
Current executable set to '/Users/kim/projects/lean/aesop/.lake/build/bin/aesop_test_executable' (arm64).
(lldb) run
Process 15929 launched: '/Users/kim/projects/lean/aesop/.lake/build/bin/aesop_test_executable' (arm64)
Process 15929 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0xf500000000000000)
    frame #0: 0x000000010061ea4c aesop_test_executable`_init_l_Aesop_Frontend_Feature_elab___closed__7 + 28
aesop_test_executable`:
->  0x10061ea4c <+28>: ldr    w8, [x19]
    0x10061ea50 <+32>: cmp    w8, #0x1
    0x10061ea54 <+36>: b.lt   0x10061ea70               ; <+64>
    0x10061ea58 <+40>: add    w8, w8, #0x1
Target 0: (aesop_test_executable) stopped.
(lldb) bt
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0xf500000000000000)
  * frame #0: 0x000000010061ea4c aesop_test_executable`_init_l_Aesop_Frontend_Feature_elab___closed__7 + 28
    frame #1: 0x000000010061bd30 aesop_test_executable`initialize_Aesop_Frontend_RuleExpr + 8936
    frame #2: 0x000000010063d588 aesop_test_executable`initialize_Aesop_Frontend_Tactic + 140
    frame #3: 0x000000010064f260 aesop_test_executable`initialize_Aesop_Main + 176
    frame #4: 0x000000010070ec14 aesop_test_executable`initialize_Aesop + 124
    frame #5: 0x00000001000009cc aesop_test_executable`initialize_AesopTest_Main + 124
    frame #6: 0x0000000100000a54 aesop_test_executable`main + 32
    frame #7: 0x000000019990f154 dyld`start + 2476

Even after fixing the underlying problem, we can't merge this as a regression test PR without adjusting the testDriver set up. We want to both run the executable, and build the AesopTest library, and as far as I can see this isn't currently possible.

[hargoniX]

The extracted closed term here is:

def Aesop.Frontend.Feature.elab._closed_7 : obj :=
  let x_1 : obj := Aesop.Frontend.Feature.elab._closed_4;
  let x_2 : obj := 0;
  let x_3 : obj := Array.get ◾ x_1 x_2 ◾;
  dec x_1;
  ret x_3

and _closed_4 is:

def Aesop.Frontend.Feature.elab._closed_4 : obj :=
  let x_1 : obj := ctor_0[List.nil];
  let x_2 : obj := Array.mk ◾ x_1;
  ret x_2

so it is indexing into an empty array. I'm very certain that I have seen this issue on the core issue tracker before but I cannot find it anymore :(. The trivial fix is of course to disable the closed term extractor here. Alternatively we could fiddle with the code until this doesn't happen anymore or wait for the new code generator.

[JLimperg]

#183 fixes the segfault by disabling extraction for Aesop.Frontend.Feature.elab.

Leaving this PR open for the regression test.

[kim-em]

This does add 1:23 minutes to the CI time, which I don't like. But I also don't like this breakage!

[TwoFX]

so it is indexing into an empty array. I'm very certain that I have seen this issue on the core issue tracker before but I cannot find it anymore :(.

@hargoniX Could you be looking for leanprover/lean4#5188?

[hargoniX]

Yes!

[kim-em]

Rather than add to the CI time, let's do this daily in Mathlib, where we already have infrastructure for daily CI runs for expensive jobs.

leanprover-community/mathlib4#19755