Jean-Christophe Léchenet
Jean-Christophe Léchenet
On Coq 8.9, with coq-equations version 1.2 beta2, ``` From Equations Require Import Equations. Require Import Vector. Derive DependentElimination for t. Anomaly "Uncaught exception Reduction.NotArity." ``` This seems to occur...
If we try to call an export function, we do not get a clear message "cannot call an export function". Instead, we can get: - an assertion false in `regalloc.ml`...
The following program ``` export fn main (reg u64 i) { stack u8[2] a; a[1] = i; } ``` triggers ``` Fatal error: exception File "src/toEC.ml", line 380, characters 55-61:...
Calling the ARM-version of the compiler on the program ``` export fn main (reg u64 state) { } ``` returns ``` "", line 1 (0) to line 3 (1): internal...
I was playing with a toy example (on the `glob_array3` branch) and get the error in the title. Probably, the example makes no sense, but I was asked to report...
It was decided to release two versions in a short period of time. The first one, called "jasmin 0" (finally named 21.0) will contain what is currently in master. It...
Currently, the compilation of `jasminc` depends on proof files (psem.v, asmgen.v, linear_proof.v, etc.). This is due to the algorithmic and proof parts being mixed in such files. Extracting these parts...
It would be nice to have emacs/vim/sublime... support. Is there already something lying around somewhere? What kind of features can we have without doing something too complex?
One big advantage would be to have the CI results reported inside the PRs. A first try was attempted in https://github.com/jasmin-lang/jasmin/pull/96 but reverted in https://github.com/jasmin-lang/jasmin/pull/105 due to some limitations of...
The code and the proof seem too complex. We need to take a close look to know how to improve the current situation.