Diagnosing timeout

Stream: general

[Bhavik Mehta]

I'm getting a confusing deterministic timeout - with the last line of my proof there's a timeout but without it there isn't, and if I reorder the proof to have a different last line, still the last line gives a timeout. I haven't used anything like simp or tidy, and I'm pretty sure there shouldn't be any difficult typeclass searches either. What sort of thing could I do to figure out why it's timing out? (I can't really post an MWE since it's on top of thousands of lines of topos code but the proof is:

def sheaf_exponential (A : C) (s : sheaf C j) : sheaf C j :=
{ A := exp A s.A,
  unique_extend := λ B B' m f' d,
  begin
    haveI := @dense_prod_map_id _ _ _ _ j _ A _ _ m d,
    refine ⟨⟨⟨cchat (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).1.1.1, _⟩⟩, _⟩,
    { rw ← exp_transpose_natural_left,
      rw (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).1.1.2,
      exact ((exp.adjunction _).hom_equiv _ _).right_inv f' },
    rintro ⟨a, ha⟩,
    have z : limits.prod.map (𝟙 A) m ≫ unhat a = unhat f',
      rw [← exp_transpose_natural_left_symm m a, ha],
    rw ← (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).2 ⟨unhat a, z⟩,
    congr,
    symmetry,
    refine ((exp.adjunction A).hom_equiv _ _).right_inv a,
  end
}

[Bhavik Mehta]

I'm not sure if it makes a difference but the proof of dense_prod_map_id is currently sorry

[Bhavik Mehta]

and without the final line of the proof, it's very quick to show me the tactic state

[Reid Barton]

are there other fields of sheaf you haven't provided?

[Bhavik Mehta]

Nope

[Reid Barton]

You can try turning on various trace flags, and see whether anything looks obviously out of control. Otherwise, I am afraid it's not easy to tell what's going on

[Reid Barton]

One possibility is that you actually have a type error and Lean is going on an unfolding spree to see if it can be reduced away

[Bhavik Mehta]

Are there any trace flags I should try first? trace.class_instances didn't seem out of control

[Bhavik Mehta]

Reid Barton said:

One possibility is that you actually have a type error and Lean is going on an unfolding spree to see if it can be reduced away

This makes sense, but if I reorder the proof (eg changing the have z to a suffices) there's no type error for the alternative last line

[Bhavik Mehta]

For clarity, by reordered proof I mean:

def sheaf_exponential (A : C) (s : sheaf C j) : sheaf C j :=
{ A := exp A s.A,
  unique_extend := λ B B' m f' d,
  begin
    haveI := @dense_prod_map_id _ _ _ _ j _ A _ _ m d,
    refine ⟨⟨⟨cchat (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).1.1.1, _⟩⟩, _⟩,
    { rw ← exp_transpose_natural_left,
      rw (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).1.1.2,
      exact ((exp.adjunction _).hom_equiv _ _).right_inv f' },
    { rintro ⟨a, ha⟩,
      suffices z : limits.prod.map (𝟙 A) m ≫ unhat a = unhat f',
        rw ← (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).2 ⟨unhat a, z⟩,
        congr,
        symmetry,
        refine ((exp.adjunction A).hom_equiv _ _).right_inv a,
      rw [← exp_transpose_natural_left_symm m a, ha],
    }
  end
}

[Bhavik Mehta]

In both cases commenting out the last line (in the latter case, just the ha) tells me quickly that the goal isn't solved and there's no other errors

[Reid Barton]

maybe set_option trace.type_context.is_def_eq true

[Bhavik Mehta]

Doesn't seem to be crazy, one of the rw gives a pretty long trace but most of it says success

[Kevin Buzzard]

Post a MWE anyway. Seriously. Of the form "download this branch of this repo, and look at this line in this file". When people did this in the past I just thought they were taking the mickey. But now with leanproject it's much easier.

[Reid Barton]

Well, something must be happening where Lean starts taking time.

[Reid Barton]

In the past I have occasionally resorted to running Lean in a debugger, then stopping it at a random point and looking at the trace

[Bhavik Mehta]

Kevin Buzzard said:

Post a MWE anyway. Seriously. Of the form "download this branch of repo, and look at this line in this file". When people did this in the past I just thought they were taking the mickey. But now with leanproject it's much easier.

The final line in https://github.com/b-mehta/topos/blob/sheaf/src/sheaf.lean - download the sheaf branch of the repo. (It's not particularly minimal)

[Bhavik Mehta]

Reid Barton said:

In the past I have occasionally resorted to running Lean in a debugger, then stopping it at a random point and looking at the trace

How could I do this?

[Bhavik Mehta]

If I add another line (eg simp) before the end, it says the tactic state is goals accomplished and the simp fails with match failed, no goals; and this happens quickly

[Sebastien Gouezel]

My guess is that you should try to fill in the sorry of dense_prod_map_id: it is not a Prop, so what you put in there is important.

By the way, all these classes (dense, closed) are not Props because is_iso is not Prop either. Does it really create problems to turn is_iso into a Prop, just requiring the existence of an inverse -- and having a convenience function is_iso.inverse that would pull the inverse out of choice?

[Johan Commelin]

This is the big "category_theory uses data, not Props" question...

[Johan Commelin]

The same thing with has_limits etc...

[Bhavik Mehta]

Yeah I think it has to be all or nothing - we've got to have everything as a Prop or everything as data otherwise things won't play well with each other

[Sebastien Gouezel]

If the data is not unique, then I understand you need to keep the data and record the way it is constructed. But when the data is unique like the inverse, I don't see the point.

[Bhavik Mehta]

In some cases, the data might only be unique up to (unique) isomorphism, but also in category theory (and topos theory) we often try to avoid using choice, so just the existence of a unique object isn't enough

[Bhavik Mehta]

It's also reasonably common to take "has limits" in category theory to mean "we are given a particular choice of limit for every diagram", which matches lean's current definition

[Bhavik Mehta]

eg just after Lemma A1.2.1 in the Elephant

[Reid Barton]

Only very picky people and theorem provers would consider "having limits" to mean a choice of limits.

[Bhavik Mehta]

I won't tell PTJ you called him picky :P

[Bhavik Mehta]

I'm pretty sure this is the convention in MM as well

[Reid Barton]

metamath?

[Bhavik Mehta]

Maclane-Moerdijk

[Reid Barton]

I think this is mainly in the eye of the beholder

[Reid Barton]

Just like, "obviously", most category theory texts mean $\mathcal{U}$-small category for some universe $\mathcal{U}$ even if they never mention universes

[Bhavik Mehta]

Reid Barton said:

I think this is mainly in the eye of the beholder

Maybe, but it is explicitly discussed and mentioned in the Elephant

[Reid Barton]

My guess is these picky people have to rely on the fact that there is nobody even pickier who wants to dismantle their position

[Kevin Buzzard]

So I tried some preliminary investigations:

...
    congr,
    symmetry,
    have ZZZ := ((exp.adjunction A).hom_equiv _ _).right_inv a,
    unfold cchat,
    unfold unhat,
    unfold exp.adjunction at ZZZ,
    dsimp,
    dsimp at ZZZ,
    dunfold exp_transpose,
    sorry
  end

[Kevin Buzzard]

ZZZ : ⇑(is_left_adjoint.adj.hom_equiv B s.A) (⇑(equiv.symm (is_left_adjoint.adj.hom_equiv B s.A)) a) = a
⊢ ⇑(is_left_adjoint.adj.hom_equiv B s.A) (⇑(equiv.symm (is_left_adjoint.adj.hom_equiv B s.A)) a) = a

[Kevin Buzzard]

and exact ZZZ or convert ZZZ causes the timeout

[Kevin Buzzard]

So of course when you set_option pp.all true you find that the terms are different.

[Bhavik Mehta]

Bhavik Mehta said:

For clarity, by reordered proof I mean:

def sheaf_exponential (A : C) (s : sheaf C j) : sheaf C j :=
{ A := exp A s.A,
  unique_extend := λ B B' m f' d,
  begin
    haveI := @dense_prod_map_id _ _ _ _ j _ A _ _ m d,
    refine ⟨⟨⟨cchat (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).1.1.1, _⟩⟩, _⟩,
    { rw ← exp_transpose_natural_left,
      rw (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).1.1.2,
      exact ((exp.adjunction _).hom_equiv _ _).right_inv f' },
    { rintro ⟨a, ha⟩,
      suffices z : limits.prod.map (𝟙 A) m ≫ unhat a = unhat f',
        rw ← (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).2 ⟨unhat a, z⟩,
        congr,
        symmetry,
        refine ((exp.adjunction A).hom_equiv _ _).right_inv a,
      rw [← exp_transpose_natural_left_symm m a, ha],
    }
  end
}

Yeah I get a timeout as well with exact ZZZ, but with the re-ordered version of the code that version doesn't give a type error

[Bhavik Mehta]

and that doesn't explain why it's fine if you put a simp afterwards

[Bhavik Mehta]

My current hypothesis is that Sebastian's right, and the problem happens when lean is trying to make the bytecode, so I'm currently filling in the sorry

[Kevin Buzzard]

ZZZ vs goal; diff

[Bhavik Mehta]

Looking at the first diff, that's defeq by how I defined exp

[Kevin Buzzard]

There are no sorrys in ZZZ or the goal though

[Bhavik Mehta]

Hmm

[Kevin Buzzard]

Oh this is interesting

[Kevin Buzzard]

def sheaf_exponential (A : C) (s : sheaf C j) : sheaf C j :=
{ A := exp A s.A,
  unique_extend := λ B B' m f' d,
  begin
    haveI := @dense_prod_map_id _ _ _ _ j _ A _ _ m d,
    refine ⟨⟨⟨cchat (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).1.1.1, _⟩⟩, _⟩,
    { rw ← exp_transpose_natural_left,
      rw (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).1.1.2,
      exact ((exp.adjunction _).hom_equiv _ _).right_inv f' },
    { rintro ⟨a, ha⟩,
      suffices z : limits.prod.map (𝟙 A) m ≫ unhat a = unhat f',
        rw ← (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).2 ⟨unhat a, z⟩,
        congr,
        symmetry,
        exact ((exp.adjunction A).hom_equiv _ _).right_inv a,
      rw [← exp_transpose_natural_left_symm m a, ha],
      sorry,
    },
  end
}

[Kevin Buzzard]

Tactic State
goals accomplished
sheaf.lean:184:6: error
tactic failed, there are no goals to be solved
state:
no goals

[Kevin Buzzard]

the error is on the sorry, complaining that I'm apologising when I'm all done.

[Bhavik Mehta]

Right - this is the same as the simp thing I saw earlier

[Bhavik Mehta]

Really weird!

[Kevin Buzzard]

def sheaf_exponential (A : C) (s : sheaf C j) : sheaf C j :=
{ A := exp A s.A,
  unique_extend := λ B B' m f' d,
  begin
    haveI := @dense_prod_map_id _ _ _ _ j _ A _ _ m d,
    refine ⟨⟨⟨cchat (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).1.1.1, _⟩⟩, _⟩,
    { rw ← exp_transpose_natural_left,
      rw (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).1.1.2,
      exact ((exp.adjunction _).hom_equiv _ _).right_inv f' },
    { rintro ⟨a, ha⟩,
      suffices z : limits.prod.map (𝟙 A) m ≫ unhat a = unhat f',
        rw ← (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f')).2 ⟨unhat a, z⟩,
        congr,
        symmetry,
        exact ((exp.adjunction A).hom_equiv _ _).right_inv a,
      rw [← exp_transpose_natural_left_symm m a, ha],
    },
    sorry
  end
}

same error

[Kevin Buzzard]

I've seen Lean in sort of this state before -- there are hidden goals. There's a tactic which makes them come out

[Bhavik Mehta]

But I don't think there are hidden goals! In all the code I've written I haven't used any . obviously or anything

[Kevin Buzzard]

Sometimes a tactic just leaves some hidden goals behind by accident

[Bhavik Mehta]

True

[Patrick Massot]

Bhavik Mehta said:

My current hypothesis is that Sebastian's right, and the problem happens when lean is trying to make the bytecode, so I'm currently filling in the sorry

You probably mean Sébastien here. I don't know why Zulip doesn't use accents here, but the ASCII version is already enough to disambiguate between Sebastian working on Lean4 and Sebastien working on calculus and analytic functions

[Kevin Buzzard]

I can't remember the name of the tactic which makes the hidden goals appear :-(

[Mario Carneiro]

recover?

[Kevin Buzzard]

Yeah that's the one. OK I am going back to blaming the sorried data. The problem isn't the exact, it's when Lean is putting everything together afterwards.

[Bhavik Mehta]

Patrick Massot said:

Bhavik Mehta said:

My current hypothesis is that Sebastian's right, and the problem happens when lean is trying to make the bytecode, so I'm currently filling in the sorry

You probably mean Sébastien here. I don't know why Zulip doesn't use accents here, but the ASCII version is already enough to disambiguate between Sebastian working on Lean4 and Sebastien working on calculus and analytic functions

Oops, yeah, thanks!

[Reid Barton]

Or as I call them, Sebasti∀n and Sebasti∃n.

[Mario Carneiro]

Maybe it should be renamed #recover; it's not intended for leaving in proof scripts because it's pretty expensive and usually indicates a bug in another tactic

[Mario Carneiro]

Another Mario has appeared on the chat, so maybe I need to start going by Mário

[Patrick Massot]

We lost track of how many Kevin we have a long time ago.

[Bhavik Mehta]

Hopefully I'll be safe for a while

[Bhavik Mehta]

Or maybe I should hope for the opposite

[Reid Barton]

Bhavik Mehta said:

Reid Barton said:

In the past I have occasionally resorted to running Lean in a debugger, then stopping it at a random point and looking at the trace

How could I do this?

Depends on your platform I suppose, but I just run lean inside gdb

[Reid Barton]

from the command line

[Bhavik Mehta]

Kevin Buzzard said:

Yeah that's the one. OK I am going back to blaming the sorried data. The problem isn't the exact, it's when Lean is putting everything together afterwards.

This isn't it... I filled in the sorry

[Bhavik Mehta]

For those experimenting, I've pushed the updated version - same file

[Bhavik Mehta]

Further confusing this, I've got two other defs which construct a sheaf and they don't have the same problem...

[Kevin Buzzard]

This is worth more investigation. I've had quite a busy day today and I've got another one tomorrow but I hope to find the time to look at this again, it's not like anything I've seen before which is why I find it interesting. Can you make a branch with the error so it doesn't get lost?

[Bhavik Mehta]

Will do!

[Kevin Buzzard]

Screencast-2020-05-01-203515.mp4

[Bhavik Mehta]

If anyone knows of any workarounds that might work I'd find that useful as well

[Kevin Buzzard]

@Mario Carneiro @Gabriel Ebner @Reid Barton what is going on here?

[Kevin Buzzard]

Sometimes it takes forever to time out, sometimes it's quick, but it never works

[Kevin Buzzard]

Restarting Lean just makes it think forever and then time out with the error

excessive memory consumption detected at 'expression equality test' (potential solution: increase memory consumption threshold)

[Mario Carneiro]

I am guessing the term is bad in some way, and the kernel has decided to unfold everything as a result

[Bhavik Mehta]

Kevin Buzzard said:

the error is on the sorry, complaining that I'm apologising when I'm all done.

How does that explain this?

[Reid Barton]

Writing sorry when there are no goals is an error, right?

[Reid Barton]

I didn't follow what Kevin was seeing in his video.

[Reid Barton]

In particular, it looks like the tactic block is succeeding but then the resulting term is somehow defective.

[Reid Barton]

I suggested set_option trace.type_context.is_def_eq true before but I think it really should have been the one with detail.

[Reid Barton]

Try turning that on and running lean on your file from the command line

[Reid Barton]

I used these flags today and I think is_def_eq only displays the unification problems, not the trace of trying to solve them.

[Bhavik Mehta]

I didn't realise the def was underlined blue! That's the one with the long trace - and it fits with the idea that there's an issue creating the term

[Bhavik Mehta]

I can't figure out what the issue is though

[Bhavik Mehta]

Here's the trace: https://gist.github.com/b-mehta/88525a9eb2c41c23e414d9bb30c650fb

[Reid Barton]

The question is whether, when you run Lean from the command line, you get trace output continuously or whether it just stops at some point.

[Reid Barton]

If it just stops, clearly it is doing something and the game is to figure out what trace option will make it print more stuff.

[Bhavik Mehta]

In vscode it stops and says deterministic timeout, I'm running on command line now

[Bhavik Mehta]

Ah! It runs for a while and then stops

[Bhavik Mehta]

and my memory gets filled up

[Bhavik Mehta]

Is there a list of what each trace option does?

[Reid Barton]

Well, there's the autocomplete menu...

[Reid Barton]

I would just run it in a debugger at this point

[Bhavik Mehta]

The autocomplete menu doesn't give information about what the difference between each trace option is though

[Reid Barton]

oh, I guess only some things are documented then

[Bhavik Mehta]

Reid Barton said:

I would just run it in a debugger at this point

How do I go about doing this? I'm not familiar with gdb

[Reid Barton]

Probably something like gdb --args lean myfile.lean, then type r and ctrl-C when it starts thinking for a long time

[Reid Barton]

then bt to see the stack trace

[Bhavik Mehta]

$ gdb --args lean ./src/sheaf.lean
GNU gdb (GDB) 8.3
Copyright (C) 2019 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Type "show copying" and "show warranty" for details.
This GDB was configured as "x86_64-apple-darwin17.7.0".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<http://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
    <http://www.gnu.org/software/gdb/documentation/>.

For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from lean...

warning: Could not open OSO archive file "/Users/travis/.rustup/toolchains/stable-x86_64-apple-darwin/lib/rustlib/x86_64-apple-darwin/lib/liballoc-089d48ff1bba5f70.rlib"

warning: Could not open OSO archive file "/Users/travis/.rustup/toolchains/stable-x86_64-apple-darwin/lib/rustlib/x86_64-apple-darwin/lib/libbacktrace_sys-b0895307a49d7b98.rlib"

warning: Could not open OSO archive file "/Users/travis/.rustup/toolchains/stable-x86_64-apple-darwin/lib/rustlib/x86_64-apple-darwin/lib/libcompiler_builtins-35232c4af1148867.rlib"

warning: Could not open OSO archive file "/Users/travis/.rustup/toolchains/stable-x86_64-apple-darwin/lib/rustlib/x86_64-apple-darwin/lib/libcore-f948d62f596dcd3d.rlib"

warning: Could not open OSO archive file "/Users/travis/.rustup/toolchains/stable-x86_64-apple-darwin/lib/rustlib/x86_64-apple-darwin/lib/libpanic_unwind-cb02f3c2aa14313b.rlib"

warning: Could not open OSO archive file "/Users/travis/.rustup/toolchains/stable-x86_64-apple-darwin/lib/rustlib/x86_64-apple-darwin/lib/librustc_demangle-136c67c44acb8989.rlib"

warning: Could not open OSO archive file "/Users/travis/.rustup/toolchains/stable-x86_64-apple-darwin/lib/rustlib/x86_64-apple-darwin/lib/libstd-d4fbe66ddea5f3ce.rlib"

warning: Could not open OSO archive file "/Users/travis/.rustup/toolchains/stable-x86_64-apple-darwin/lib/rustlib/x86_64-apple-darwin/lib/libunwind-5751ec7e6e80fbea.rlib"
(No debugging symbols found in lean)
(gdb)

[Reid Barton]

that's probably okay, type r anyways

[Bhavik Mehta]

(gdb) r
Starting program: /Users/bmehta/.elan/bin/lean ./src/sheaf.lean
Unable to find Mach task port for process-id 31753: (os/kern) failure (0x5).
 (please check gdb is codesigned - see taskgated(8))

[Reid Barton]

oh maybe your OS is broken

[Reid Barton]

Rough luck

[Bhavik Mehta]

uh oh

[Reid Barton]

I mean, this error is probably by design

[Reid Barton]

but it seems to be preventing you from what you want to do

[Reid Barton]

Is there some way you can make Lean's life easier by breaking up the definition?

[Alex J. Best]

You can (and need to) codesign gdb on osx, there should be instructions online.

[Bryan Gin-ge Chen]

I tried to get gdb running on macOS and had no luck. You can use lldb though. The steps are very similar to what Reid suggested with gdb.

[Bryan Gin-ge Chen]

The lldb experience is a bit inferior right now since you can't use this pretty-printing script.

[Reid Barton]

Ah thanks Bryan, I should have remembered that lldb is OSX for gdb.

[Alex J. Best]

What didn't work for you @Bryan Gin-ge Chen ? The codesigning or something else? I just followed https://gist.github.com/hlissner/898b7dfc0a3b63824a70e15cd0180154 and it worked (I had to sudo killall taskgated in step 9) but other than that my gdb no longer complains.

[Bryan Gin-ge Chen]

I'm using 10.14 so when I went through this in July, I tried the 10.12 and later instructions that are linked at the top of that gist. I don't remember what failed exactly, but it seems like there are various modifications people suggest in the comments which I might try now eventually.

[Alex J. Best]

Ah, 10.13 here.

[Bhavik Mehta]

$ lldb -- lean ./src/sheaf.lean
(lldb) target create "lean"
Current executable set to 'lean' (x86_64).
(lldb) settings set -- target.run-args  "./src/sheaf.lean"
(lldb) r
Process 36768 launched: '/Users/bmehta/.elan/bin/lean' (x86_64)
Process 36768 stopped
* thread #2, stop reason = exec
    frame #0: 0x0000000100c5f19c dyld`_dyld_start

Presumably I'm misunderstanding how to do something here...

[Bhavik Mehta]

Kevin Buzzard said:

This is worth more investigation. I've had quite a busy day today and I've got another one tomorrow but I hope to find the time to look at this again, it's not like anything I've seen before which is why I find it interesting. Can you make a branch with the error so it doesn't get lost?

I'll move my work to a different branch, and keep that branch fixed. That is, the error is (and will remain) https://github.com/b-mehta/topos/blob/sheaf/src/sheaf.lean#L261

[Bryan Gin-ge Chen]

@Bhavik Mehta enter r again after that. For whatever reason lldb immediately pauses the program when it starts.

[Reid Barton]

or c maybe?

[Sebastian Ullrich]

AFAIR, debugging through elan is a bad idea

[Sebastian Ullrich]

Try elan run lldb -- lean ... instead

[Reid Barton]

Oh hmm, that makes sense but I also seem to recall it just working for me. But maybe I invoked the lean binary directly, not sure.

[Sebastian Ullrich]

It might work, but for one, you can't start "lean" (actually elan) using s and then set a breakpoint on a Lean function, since you're still in the wrong process.

[Sebastian Ullrich]

Or set a breakpoint before s or r, in fact

[Bhavik Mehta]

$ elan run lldb -- lean src/sheaf.lean
error: toolchain 'lldb' is not installed

[Bryan Gin-ge Chen]

elan requires you to enter the name of the toolchain you want to use e.g. stable or nightly or leanprover-community-lean-3.9.0 before the command. I think you may be better off giving the path to the Lean binary though. You can find that out using elan which lean.

[Reid Barton]

Does elan exec lean?

[Bhavik Mehta]

Bryan Gin-ge Chen said:

Bhavik Mehta enter r again after that. For whatever reason lldb immediately pauses the program when it starts.

This worked for me! Not entirely sure what to do with this though

[Bhavik Mehta]

Reid Barton said:

Probably something like gdb --args lean myfile.lean, then type r and ctrl-C when it starts thinking for a long time

Here's the output from this:

[type_context.is_def_eq_detail] [3]: sheaf' ?m_1 ?m_5 =?= sheaf' C j
[type_context.is_def_eq_detail] [4]: sheaf' =?= sheaf'
r
Process 64955 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = signal SIGSTOP
    frame #0: 0x00007fff6c473a16 libsystem_kernel.dylib`__psynch_cvwait + 10
libsystem_kernel.dylib`__psynch_cvwait:
->  0x7fff6c473a16 <+10>: jae    0x7fff6c473a20            ; <+20>
    0x7fff6c473a18 <+12>: movq   %rax, %rdi
    0x7fff6c473a1b <+15>: jmp    0x7fff6c46aae9            ; cerror_nocancel
    0x7fff6c473a20 <+20>: retq
Target 0: (lean) stopped.
(lldb) bt
* thread #1, queue = 'com.apple.main-thread', stop reason = signal SIGSTOP
  * frame #0: 0x00007fff6c473a16 libsystem_kernel.dylib`__psynch_cvwait + 10
    frame #1: 0x00007fff6c63c589 libsystem_pthread.dylib`_pthread_cond_wait + 732
    frame #2: 0x00007fff6a277cb0 libc++.1.dylib`std::__1::condition_variable::wait(std::__1::unique_lock<std::__1::mutex>&) + 18
    frame #3: 0x0000000100230dab lean`lean::mt_task_queue::wait_for_finish(std::__1::shared_ptr<lean::gtask_cell> const&) + 523
    frame #4: 0x00000001000055ca lean`main + 9914
    frame #5: 0x00007fff6c323015 libdyld.dylib`start + 1
    frame #6: 0x00007fff6c323015 libdyld.dylib`start + 1
(lldb)

[Bryan Gin-ge Chen]

(deleted)

[Sebastian Ullrich]

Ah, elan run doesn't actually change the path, that's disappointing. We're planning to use it for Lean 4 development, so I hoped I could invoke gdb that way. gdb/lldb $(elan which lean) should work, however.

[Bhavik Mehta]

Apologies for the presumably stupid questions, this sort of thing is very much outside my wheelhouse

[Reid Barton]

Seems like lldb is showing you the wrong thread. This just worked for me on linux...

[Reid Barton]

Okay, I managed to build your project and get a stack trace, and it's 400 levels deep in is_def_eq stuff

[Reid Barton]

It's possible I didn't wait long enough before interrupting it though

[Bhavik Mehta]

I kept the type_context.is_def_eq_detail, and interrupted when it stopped printing lines

[Bhavik Mehta]

there were ~3612 lines

[Reid Barton]

Specifically there's a lot of lean::type_checker::is_def_eq_core(lean::expr const&, lean::expr const&) involved

[Reid Barton]

It's all inside lean::abstract_nested_proofs_fn::visit(lean::expr const&)

[Reid Barton]

Is this the kernel or the elaborator?

[Bhavik Mehta]

I have no idea

[Reid Barton]

Looks like it is the kernel

[Patrick Stevens]

Bhavik Mehta said:
I'll move my work to a different branch, and keep that branch fixed. That is, the error is (and will remain) https://github.com/b-mehta/topos/blob/sheaf/src/sheaf.lean#L261

By the way, this is what tags are for, rather than branches - branches are inherently mutable and tags are inherently immutable

[Bhavik Mehta]

TIL, thanks

[Bhavik Mehta]

I've got the proof to work! I'm not entirely sure what fixed it, but here's my current guess: sheaf is defined like this:

structure sheaf' :=
(A : C)
(unique_extend : Π {B B'} (m : B' ⟶ B) f' [closure.dense j m], unique {f : B ⟶ A // m ≫ f = f'})

def forget_sheaf : sheaf'.{v} C j → C := sheaf'.A

def sheaf := induced_category C (forget_sheaf C j)

instance sheaf_category.category : category (sheaf C j) := induced_category.category _
def forget : sheaf C j ⥤ C := induced_functor _

The change I made was to have a named constructor and deconstructors for sheaf, and then make sheaf irreducible

[Reid Barton]

Weird/interesting

[Reid Barton]

We could just make induced_category itself do that, I suppose

[Reid Barton]

but I don't see why it would have mattered

[Bhavik Mehta]

I can't say for sure that that was the cause but I think it was this. I also have a suspicion that there was some weirdness going on with my (local) cartesian closed instances but I couldn't confirm it...

[Bhavik Mehta]

I'm getting essentially the same problem as in the original post here, but in a very different context. Specifically, the end of the proof seems to work fine, but I get a deterministic timeout on the lemma statement and nowhere else. Putting a sorry before the end says no goals, and there's no timeout. recover gives nothing helpful. The statement isn't building any data - it's a proof of function.surjective, and it's a lemma. Further, importing this file gives a timeout at the import line, and anything transitively imported through it doesn't appear (that is, A is imported by B which is imported by C, and B has this weird proof; imports from A aren't recognised in C), but again adding a sorry before the end of the proof makes the transitive imports work again.

[Bhavik Mehta]

I haven't been able to minimise, but you can replicate this with https://github.com/leanprover-community/mathlib/blob/really-flat/src/category_theory/limits/filtered_colimit_commutes_finite_limit2.lean

[Bhavik Mehta]

and you can get the import weirdness by looking in https://github.com/leanprover-community/mathlib/blob/really-flat/src/category_theory/limits/flat.lean on that same branch

[Bhavik Mehta]

Wait, the import strangeness isn't happening for me now...

[Bhavik Mehta]

oh it's happening again, I think there were old oleans

[Bhavik Mehta]

but building the file using lean --make doesn't give a timeout

[Kevin Buzzard]

I don't have any problems with the really-flat branch -- i.e. I can't reproduce. I checked it out, got oleans from azure, built category_theory.limits.filtered_colimit_commutes_finite_limit2 on the command line, opened it in VS Code and I see no errors either in the command line build or on VS Code. Maybe nuke all olean files, get them from azure and then build?

[Kevin Buzzard]

Similarly I have no problems with category_theory.limits.flat, no warnings or errors in VS Code. This is commit 61a478271e967097e3d82819b2f6f7e8c04f2932. Hopefully happiness is just around the corner for you :-)

[Bhavik Mehta]

Huh, I guess what's happening is that azure builds them from command line where the timeout doesn't happen, and if you download the oleans it all works fine