Stream: Coq devs & plugin devs

Topic: motivation for native implementations

view this post on Zulip Jason Gross (Aug 09 2020 at 22:41):

I see "We propose an alternative approach, initiated by Benjamin Grégoire after having hit memory limits when defining terms representing proof traces from SMT solvers, which consists in extending COQ’s terms with primitive data types like integers and persistent arrays, along with operators, and axiomatizing their equational theory" in Is there an extended description of these memory limit troubles anywhere? (cc @Maxime Dénès )

view this post on Zulip Maxime Dénès (Aug 10 2020 at 10:03):

I'm not sure if Benjamin wrote something concrete about it, but IIRC they were working with Chantal Keller. The trouble was simple: with non-native representation, they could not even allocate the term corresponding to the resolution trace.

Last updated: Oct 21 2021 at 20:02 UTC