Karl Palmskog
Karl Palmskog
Consider the following `sertop` session with the latest SerAPI from the `v8.10` branch (formatted for readability and with unnecessary output removed): ``` (Add () "Notation \"[ 'arg[' ord ]\" :=...
We want to be able to serialize and deserialize environments with elaborated and fully typed kernel terms (`Constr.t`). More specifically, we want to be able to serialize (relevant data from)...
The `!pinned` flag is currently used in the version-tracked opam package definition (`coq-serapi.opam`). However, this flag seemingly causes CI failures in the upstream opam repository, so it should never be...
I'm trying to set up code for serialization via `sercomp` of some proof goal information, but am running into issues. Consider the following example (`pi.v`): ```coq From mathcomp Require Import...
I'm a big fan of the "windowed mode", which essentially gives a display like Proof General. However, with a big proof context that doesn't fully fit on the screen, the...
Consider a Coq project organized like this (assume `-Q theories Test`): ``` theories/ ├── A │ └── A.v └── B └── A.v ``` If I call Alectryon as a coqdoc...
#### Description of the problem The vo files produced by `coqc` are often relatively large. For example, the Stdlib binary files on Coq 8.15 and 8.16 are around 100 MB,...
Currently, Verdi's file operation semantics assumes a stable and atomic storage, which is unrealistic and has led to bugs like uwplse/verdi-raft#51. One option to address this is to connect the...
To push the boundaries for how verified distributed systems can be, we would like to use [VST](https://github.com/PrincetonUniversity/VST) (to refine handlers to C) and CompCert to verify Verdi node handlers down...
Several parts of the Verdi [shims](https://github.com/DistributedComponents/verdi-runtime) (currently based on OCaml) can be specified and verified down to machine code, for example using [VST](https://github.com/PrincetonUniversity/VST). The current limitation is that there is...