Armaël Guéneau
Armaël Guéneau
The current implementation is relatively insane for no good reasons, except Ltac limitations. It would be interesting to see if everything can be simplified by re-implementing the library using Ltac2.
If I run `cargo creusot` and it terminates successfully, then running `cargo creusot why3 ide` immediately terminates "successfully" without launching why3ide. This had me scrambling for a while trying to...
Thanks to @bclement-ocp we'll soon have redistribuable binary builds of alt-ergo to use in `creusot setup`. (cf https://github.com/OCamlPro/alt-ergo/pull/1045). Before that we need to upgrade creusot's testsuite to use the latest...
Two testsuite quirks reported by @xldenis: 1. `cargo test --test why3` seems to always rebuild the `git2` crate, it'd be nice to understand why 2. `cargo test --test ui` takes...
Would be nice :).
Testing locally with a `git daemon` server serving `/tmp/cal` (`git daemon --verbose --export-all --enable=receive-pack`) ``` $ ./_build/default/caldav --admin-password=coolpwd --host=localhost --http=8080 --remote=git://localhost:9418/tmp/cal --tofu 2024-01-28 20:09:09 +01:00: INF [tcpip-stack-socket] Dual IPv4 and...
I'm compiling the server from the latest commit of the git repository. Testing the server with a basic local setup (git repository served at `localhost:9418/tmp/cal` by git-daemon, caldav served at...
Using memgraph with js_of_ocaml currently raises a few warnings because of the dependency on unix (for `Dot.to_file`). It would be slightly cleaner to avoid depending on unix in the core...
Trying to send emails with startTLS (on port 587) does not work; rss_to_email crashes in the `Mail.send_mails` function with: ``` run: internal error, uncaught exception: End_of_file ```
A fresh run of the tool fails with: ``` run: internal error, uncaught exception: (Sys_error "feed_datas.sexp: No such file or directory") ``` As a workaround, doing `touch feed_datas.sexp` solves the...