Stream: Coq users

Topic: Testing with multiple OCaml versions


view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:00):

But we will have to also support 4.10.2 / 4.12 for M1 folks (including, soon, me); luckily, I don't (yet) see us using Alectryon locally, but this will require some CI effort on testing an extra configuration.

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:00):

well, I would argue that testing with different OCaml versions is good anyway, similar to using both coq_makefile for dev and Dune in CI

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:01):

Generally, libraries and plugins absolutely need to, "applications" can be more closed world.

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:02):

(at least that's the Haskell experience)

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:03):

I guess the main concern is bugs in plugins that are version-dependent, so in principle we'd have to redo the full CI on both versions?

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:03):

when you develop open source stuff to be consumed by "everyone" for purposes you haven't thought of, that's a bit different from "applications" I think. So sure, if you have very specific "customers" you can do the whole thing with lock files...

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:03):

I'd count that as "libraries"

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:04):

While eg the seL4 proofs are closer to "applications"

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:05):

Even if it's true that they could have more clients than a typical application, in principle.

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:05):

Also you're entitled to care more for open-source libraries than proprietary applications!

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:06):

in a world hopefully soon to arrive ("open science"), researchers will be forced by their grants to not needlessly lock down their artifacts and go full library, even for narrow formalizations

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:09):

I’m a fan of open science, but the Coq community _might_ like to enable verifying industrial software, even if that’s closed-source. I guess BSD-like licenses signal openness to that :-)

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:09):

anyway, sorry for dragging us into such a wild OT!

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:10):

I broke off the topic a bit to fix that. I guess we can move to Coq users also.

view this post on Zulip Notification Bot (Nov 16 2021 at 14:11):

This topic was moved here from #Coq Platform devs & users > Testing with multiple OCaml versions by Karl Palmskog

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:14):

@Paolo Giarrusso at the risk of igniting flames, I find it hard to understand how industrial verification works out when everything is kept under wraps. If people are not allowed to actually build/see specs & proofs, you will be forced to trust company and possibly auditors, as usual

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:16):

I’ll get to that in a sec… on the “versions” thread: on more concrete questions, how often do proofs break on a specific OCaml version? I guess it’s mostly “build fails on some step”.

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:16):

at the very least it would make sense if some core specs & library is made public and vetted, and then a customer might be allowed to reduce their TCB to that

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:16):

I don’t disagree!

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:17):

the main failures I see with OCaml are when your proofs and specs depend on OCaml plugins, and with the build system and possibly extracted code and so on. And native_compute!

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:17):

TCB-wise, all I _can_ say is that our C++ axioms are already public, even if under the license you don’t like

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:19):

and as a rule I only try to say things that are already public — for instance, many of us come from academia so we’re aware of those kinds of questions

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:19):

well, is there a public axiom validation? E.g., empirical evidence this actually capture what C++ compilers are doing, etc.

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:21):

not exactly the best analogy, but I thought the validation of the ELF formalization was nice: https://www.cl.cam.ac.uk/~pes20/rems/papers/oopsla-elf-linking-2016.pdf

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:22):

I’m pretty confident you would not yet be satisfied

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:23):

not by the public material, at least — and I’m not going to make claims about any private material, because I can’t, and because you wouldn’t (and shouldn’t) believe me :-)

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:24):

OK, sure, I was just asking about "does there exist something like X that is public"

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:27):

I can say that semantics is a work-in-progress, and I tried to make sure the claims are clear, and they’re probably not prominent enough yet.

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:27):

(we’re currently polishing these docs up)

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:29):

is the scope of the axioms functional/behavioral only or do you consider non-functional properties (information flow, memory space, ...)?

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:30):

thankfully, our internal setup allows us to progress on verification without a finished C++ semantics…

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:31):

I’d say functional-only

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:34):

one point that was made to me recently by a cryptocurrency insider: the cryptocurrency industry uses formal verification primarily for conflict resolution, not certainty down to bit level. So there at least, the incentives align a bit more with "open science".

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:34):

anyway, I’m not yet going to argue this semantics is “correct” yet; count this as a “release early, release often” version.

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 14:35):

“conflict resolution”? conflicts between bits or humans?

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:35):

conflicts between humans about adopting protocols and the like ("most verified wins")

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:36):

well, going from a 2000-page(?) language spec in English down to hundreds/thousands of Coq lines seems worthwhile

view this post on Zulip Karl Palmskog (Nov 16 2021 at 14:37):

also fun to see all the formal verification shilling, all the Hedera proponents are seemingly perpetually excited about Karl Crary's Coq formalization of a protocol Hedera (supposedly) uses (https://www.cs.cmu.edu/~crary/papers/2021/hashgraph.pdf)

view this post on Zulip Ana de Almeida Borges (Nov 16 2021 at 14:42):

Paolo Giarrusso said:

how often do proofs break on a specific OCaml version? I guess it’s mostly “build fails on some step”.

I have a piece of Coq code that inexplicably breaks with OCaml >= 4.10. I've been meaning to open a bug report for ages, but wanted to find a MWE, and so far that's proved too time consuming and annoying. I guess I could feed it to the minimizer...

view this post on Zulip Paolo Giarrusso (Nov 16 2021 at 18:15):

Non-minimal bug reports are IMHO better than nothing, @Ana de Almeida Borges


Last updated: Sep 26 2023 at 13:01 UTC