Mauricio Collares

If you want to solve it with implicit arguments, this is the version of extensionality I used, courtesy of a kind soul in the Agda IRC channel whose name I...

Sorry for not doing this earlier! Since I understand this exercise is in a due assignment for the PUC course, I was trying to avoid "spoilers". Here's the file: https://gist.github.com/collares/5afa808eef7f647190e0dea244e6eb50

Sorry, I now have a clue as to where I went wrong: If I use Data.Product._×_ instead of plfa.Isomorphism._×_, then I don't need any sort of extensionality for the proof....

I renamed this issue since the problem with ∀-× affects even people using the book imports, whereas my original issue was specific to using plfa.Isomorphism.× instead of Data.Product.×.

I added some logging, and found out the preflight checks stop running as soon as the first `handle_info({:poll, repetition}, project_id)` call gets executed. This makes sense, since https://github.com/bors-ng/bors-ng/blob/master/lib/worker/batcher.ex#L239 instructs GenServer...

@notriddle Any suggestions on how to proceed? The least-invasive solution to this would be to not return `:stop` in `batcher.ex`'s `handle_info({:poll, repetition}, project_id)` method if there are pending preflight checks....

`:bind` defers loading (to when you use one of the bound keys), and `:config` runs only after the package is loaded. So I think the behavior you're seeing is expected.

Hi @abo-abo! Love your emacs packages. The TL;DR is that there is no config setting that I know of to fix this. It's been a while and I don't remember...

An alternative solution would be to add 1 to the value of `rclen` instead, given that `2 * num_chunks + 6` appeared in the expression. Is there a way to...

Just saw the same problem on x86_64 with version 2.5.0. Probably intermittent. ``` FAIL: test-charpoly-check ========================= CHARPol server PLUQ : 7.79629e-05s (6.2e-05 cpu) [1] CHARPol client CHECK: 0.000102997s (4.2e-05 cpu)...