Pierre Villemot
Pierre Villemot
Printers of #211 work on many Alt-Ergo files after disabling logic detection, as in #225. However, some files still cause Dolmen to raise uncaught exceptions. For instance, on the following...
The printer feature of #211 failed to convert the following file into psmt2 format: ``` logic x : int logic y : int logic z : ('a, 'b) farray goal...
This PR adds the tests of gixsql (https://github.com/OcamlPro/gixsql) in the CI of Superbol. As you can check on my fork (https://github.com/Halbaroth/superbol-studio-oss/pull/1), only 43 out of 69 tests succeed. How it...
Cmdliner determines the option format based on the length of the option name: - For options of length 1, it uses a single dash (e.g., -f). - For options longer...
Let's imagine you have a crate, says C1, and you want to specify it. However, you **do not** want to verify the crate. I proceed as follows: 1. Add `creusot-contracts`...
I am trying to verify the IndexMap crate with the latest Creusot release (0.4.0) and I am stuck. Adding `use creusot_contracts::requires;` to the `lib.rs` file of IndexMap produces the following...
In this PR: https://github.com/geneweb/geneweb/pull/2167 I have two opam files `geneweb.opam` and `geneweb-rpc.opam`. The `zarith` package is an optional dependency of `geneweb` and a transitive dependency of `geneweb-rpc`. If I run...
This PR adds a completely new parser for the `Text Language Stolen to Wikipedia` language. TODO: - [ ] Add a recovery mode. - [ ] Support `gw` format in...
This PR optimizes a bit the request: ``` http://127.0.0.1:2317/roglo-v7?m=TT&p=* ``` You can test it with this option: ```command -cache-in-memory roglo-v7 -n_workers 0 ``` and without `-n_workers 0`. The request is...
This PR adds a search engine for Geneweb. ## Organization of the PR All the new code is located in a new library `search` within the `lib/` directory. This library...