Joseph Kiniry
Joseph Kiniry
> @ice1000 Sorry, I forgot I already committed [63972b7](https://github.com/HoTT/HoTT-Agda/commit/63972b709fa8ab8df9a581181c43b6a261b9988d) to make `core/HoTT.agda` type check on my local branch. Also, the termination checker of `2.6.0-ac38171` seems to reject new code from...
> > > @ice1000 Sorry, I forgot I already committed [63972b7](https://github.com/HoTT/HoTT-Agda/commit/63972b709fa8ab8df9a581181c43b6a261b9988d) to make `core/HoTT.agda` type check on my local branch. Also, the termination checker of `2.6.0-ac38171` seems to reject new...
> > > > > @ice1000 Sorry, I forgot I already committed [63972b7](https://github.com/HoTT/HoTT-Agda/commit/63972b709fa8ab8df9a581181c43b6a261b9988d) to make `core/HoTT.agda` type check on my local branch. Also, the termination checker of `2.6.0-ac38171` seems to...
Great; we look forward to taking it for a test drive!
Hi Sam, Hope you are doing well too. Perhaps I'll even get to come down and see you all before the end of this year. 🤞 Here is more context....
Ping @mkiniry.
External timing on the scripts presumes an empty DB. I have been using some shell scripting to narrow log messages to get the precise timings you have seen in the...
Do you believe that we have all of these bases covered in the current logging system, @dmzimmerman?
Good points @nealmcb. Being more explicit about what happened later is a good idea.