Catalin Hritcu

Is there any way to get gitdub as a free service for open source projects?

2

With GitHub deprecating their commit notification email sending service (https://developer.github.com/changes/2018-04-25-github-services-deprecation/) people like me who came to heavily rely on this feature for a lot of their GitHub repos are looking...

Now need to set FSTAR_HOME to verify examples

3

Without that I'm getting a new error: ``` $ make -C examples make: Entering directory '/home/hritcu/Projects/fstar/pub/examples' Makefile.include:11: /home/hritcu/Projects/fstar/pub/bin//../lib/fstar/gmake/fstar.mk: No such file or directory make: *** No rule to make target...

Define our logical connectives in `prop`

6

We can currently define a `prop` type in various ways, for instance: ``` type prop = a:Type0{ forall (x:a). x === () } ``` or (maybe) better: ``` abstract let...

Function subtyping at depth with "enhancements"

4

The following code works, I'm basically just giving another name to `Cons`: ``` val push : int -> list int -> Tot (s:(list int){Cons? s}) let push x xs =...

No generation of functions (verification interesting)

8

The code ``` Require Import Gen. Definition tryGenFun : Gen (nat -> nat) := arbitrary. ``` yields the following error ``` Toplevel input, characters 43-52: Error: Cannot infer the implicit...

Random missing bits: only one left semSuchThatMaybe_complete

4

Making a list of TODOs in the code we might want to fix (or at least should have a fairly good idea that we could fix): `ModuleGen.v`: ``` (* TODO:...

Setting `defNumTests` to a large number causes mutation testing to take really long, even if it takes really little with a small number. What's happening?

[Zoe might have discovered a nicer way?] there is this Declare keyword, it might be helpful You can do something like that ``` Module Type M1. Parameter X : Type....

Serious performance issue for naive red-black tree generator

2


Audit Axioms

4

Audit Axioms, try to reduce their number. ``` [hritcu@detained plugin]$ grep "Axiom\b" src/*.v grep "Axiom\b" src/*.v src/Random.v:Axiom RandomSeed : Type. src/Random.v:Axiom randomSeedInhabitant : RandomSeed. src/Random.v:Axiom randomNext : RandomSeed -> Z...