search

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link

Mortality #477

Open kaonn opened 5 years ago

kaonn commented 5 years ago

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

jonsterling commented 5 years ago

@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!

jonsterling commented 5 years ago

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!)

kaonn commented 5 years ago

I think the error is contained to the various split functions, so it shouldn't take so long to typecheck.

jonsterling commented 5 years ago

@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)

jonsterling commented 5 years ago

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.

kaonn commented 5 years ago

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.