Lasse Blaauwbroek

Add the primitive `catch_system` to the logic monad

1

This allows writing a tactical that catches (non-monadic) system exceptions during the execution of a tactic. As a proof of concept, we introduce the Ltac tactical `catch_stack_overflow`. I think that...

Cannot dynlink to the Stm in `vscoqtop`

4

The [Tactician](http://coq-tactician.github.io) plugin depends on the `coq-core.stm` library. However, it seems that this library is not linked into the `vscoqtop` executable. As such, Tactician is not functional in VsCode 2....

`Value type mismatch` when combining dynamic and compiled schemas

1

I'm getting the following counter-intuitive exception while attempting to `set` a `DynamicValue` to a field: ``` capnp.lib.capnp.KjException: capnp/dynamic.c++:591: failed: expected structValue.getSchema() == structType [pytact/graph_api.capnp:GlobalContextAddition == pytact/graph_api.capnp:GlobalContextAddition]; Value type mismatch. ```...

[Feature Request] API for async reading of packed messages

2

Currently, the API does not appear to make it possible to read a stream of messages from a socket in async mode. Ideally, there would be an interface like ```...

Proposal: Reduce dependency on file descriptors

12

Pycapnp mostly works by passing file descriptors into the capnproto c++ library. This causes some problems: - Python wrappers around file descriptors are non-functional. For example, when reading messages from...

While looking at #333, I hypothesized that upgrading Cython might solve the issue. It didn't. But upgrading should still happen at some point. This is my work in progress on...

`coq-elpi` cannot be built while it is installed

4

When I first run `opam install coq-elpi` and then `make build OCAMLWARN=` I get ``` File "./theories/derive.v", line 55, characters 0-73: Error: File derive_hook.elpi found twice in elpi.apps.derive: /coq8.16/coq-elpi/apps/derive/elpi/derive_hook.elpi, /coq8.16/_opam/lib/coq/user-contrib/elpi/apps/derive/derive_hook.elpi....

Cors related traceback on `run_async.py`

3

### Is there an existing issue for this? - [X] I have searched the existing issues ### Describe the bug I'm running Sanic as part of a larger async codebase....

It is not possible to connect to an ipv6 address using `Where_to_connect` when specifying no bind address. It errors out with `Address family not supported by protocol`. This seems to...

Compiling ``` @0xafda4797418def92; const listlist :List(List(UInt8)) = [[3]]; ``` Leads to generated code with a syntax error (partially replicated here): ``` module Reader = struct type array_t = ro MessageWrapper.ListStorage.t...