Lasse Blaauwbroek
Lasse Blaauwbroek
When executing an install command in `--verbose` mode, any messages that are printed to `/dev/stderr` by a build command are redirected to `/dev/stdout` by Opam. It would be better if...
This fixes #129 and probably also fixes #106. This is a complete hack, and among other things introduces a memory leak. However, it does mostly seem to work. There still...
I'm not sure why, but the maximum with of images is larger than the width of the text. This allows the image to grow to the right of the text....
For a course, we would like to create a custom installer of the platform (with additional packages). For windows, creating a installer exe is well-documented. It is currently not clear...
`pycapnp` is based on polling and generally sleeps for `0.01` second between polls. This means that a maximum of 100 messages per second can be exchanged. This is a significant...
If I only have `coq-core` installed, given `MyCoqFile.v` ``` Declare ML Module "ltac_plugin". ``` Running ``` coqc -noinit MyCoqFile.v ``` errors out with ``` cannot guess a path for Coq...
This is a followup on the discussion I started here: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Discharging.20proof.20states Summary: Since 8.16, the function `Cooking.expmod_constr` has disappeared due to https://github.com/coq/coq/pull/14727, which breaks my plugin. So I'd like to...
As described in https://github.com/capnproto/capnproto/issues/1542, Pycapnp is having issues with catching signals while executing long-running capnp C++ code, because Python's signal handlers are only executed outside of external code. Other libraries...
I'm happy to report that I've successfully updated the online demo of Tactician to `v8.17+lsp` (to be deployed soon, not online yet). This is actually the only version of JsCoq...
(Not sure if this is a JsCoq or coq-lsp issue.) Consider the following code: ```coq From Coq Require Import Utf8. Inductive list := | nil : list | cons :...