reflectors preserve coproducts and coequalizers #743
Conversation
|
LGTM |
| rewrite concat_pp_p in p. | ||
| apply moveR_Vp in p. | ||
| rewrite@A <- p; clear p. | ||
| (** for the next one, [rewrite@A] spins forever *) |
There was a problem hiding this comment.
Sounds like a bug in rewrite@A. Any chance you can figure out what part it spins forever in? (Perhaps with Info 1 rewrite@A ...?)
There was a problem hiding this comment.
Info 1 rewrite@A also spins forever, and doesn't produce any output when I break it. Manually copy-pasting and stepping through suggests the problem is in left_associate_concat_in, which is a bit too much magic for me to understand.
There was a problem hiding this comment.
More specifically, here's some code that spins forever (where "forever" means "until I get bored and break it"):
let lem' := preconcat_any @to_O_natural_compose in
pose proof lem' as H.
left_associate_concat_in H.
There was a problem hiding this comment.
I think you can get info to print something by doing, e.g., Info 1 try (timeout 2 <sometactic>). The timeout will make it not spin forever, and the try will cause the whole command to succeed, so Info should print things. I'll try to look into it when I get a chance, but I'm not sure when that will be.
There was a problem hiding this comment.
That still doesn't print anything here.
There was a problem hiding this comment.
That's unfortunate. Assuming it is left_associate_concat_in that's being slow: there's a @?c that should be @ ?c, if the github display is right. Any chance adding a space there fixes it?
There was a problem hiding this comment.
Otherwise, you could stick let dummy := constr:($(idtac H ":" T)$) in after let T := type of H in, and seeing what try (timeout 2 ...) prints out. That will tell us if it's spinning on some unification problem (we get a few lines, and then it spins without printing anything) or because it keeps doing the same thing over and over (we get a continuous stream of lines until the time runs out). I don't have access to a computer right now, and am about to go to sleep, but I might get a chance to take a look at it this weekend, if these suggestions don't pan out.
There was a problem hiding this comment.
Adding a space doesn't change anything. let dummy results in Cannot infer an internal placeholder of type "Type" when compiling RewriteModuloAssociativity.
I opened a dedicated issue for this: #744.
There was a problem hiding this comment.
Oh, oops, make it constr:($(idtac H ":" T; exact tt)$). I'm out of practice with tactics in terms and forgot that the tactic actually has to build something.
There was a problem hiding this comment.
Ok, that gets us somewhere. We have a continuous stream of lines which start like
(transport
(fun _ : dst = to O C ((fun x : A => g0 (f x)) a) =>
(fun _ : dst = to O C ((fun x : A => g0 (f x)) a) =>
(fun _ : dst = to O C ((fun x : A => g0 (f x)) a) =>so it does appear to be doing the same thing over and over (whatever that is).
|
I don't think this PR needs to wait on debugging |
reflectors preserve coproducts and coequalizers
where "preserve" means "map them to colimits in the subuniverse, i.e reflected colimits". The proof for coequalizers was really hard; I kind of hope I am missing something obvious that would make it easier.