RedPRL
Mortality
ncoe too mortal
split/half on line 260
https://github.com/RedPRL/redtt/blob/mortal/library/cool/sort.red
raise TooMortal on line 347
https://github.com/RedPRL/redtt/blob/mortal/src/core/Domain.ml
@kaonn Thanks for reporting this! I'm sorry that it's taking me a little longer than anticipated to look into it. Unfortunately, unleashing a couple of papers has been taking precedence of hacking for a while. I hope to get back to it soon!
I finally got around to looking at this, and it is unfortunate that it is happening so deep into a proof library that takes several minutes to typecheck. I am inclined to suggest that we should try and reduce this to something smaller, because it will not be feasible to debug a proof of this size.
(Technically, the caching support of redtt doesn't help, since if we are debugging and making changes, we need to blow away the cache every time in order to get an accurate result!)
I think the error is contained to the various split functions, so it shouldn't take so long to typecheck.
@kaonn I think you may be misunderstanding my comment --- the infeasible part is that this split function depends on about a half-hour's worth of other proofs, and it is not at all clear that the error which appears in split is not caused by a bug which made some other earlier proof evaluate to the wrong thing, etc.
Debugging something that depends on so many other proofs is like digging a hole in quicksand... To localize the error, we must have an example that doesn't depend on so much other stuff. (Unless we have a stroke of insight)
I kind of don't even want to classify as bugs things which only appear in proofs that are much more complicated than what redtt is built to withstand (== anything which takes more than 10 minutes to elaborate). The reason for this is that it is infeasible to debug such proofs -- I debug proofs by looking at intermediate subgoals etc., but the subgoals that are appearing in examples like this are all tens of thousands of lines long.
my bad, I removed the other files that are irrelevant for split. It really doesn't depend on any of the brutal proofs in merge or insert.