Set up infrastructure for monthly CVC5 data dump

[thatplguy]

Clark's group would like roughly 100 examples each month, to be uploaded to a Git repo they set up (TBD: get the repo link). Each example should include the SMT queries involved, as well as sufficient metadata to produce the code that generated the queries (code base, file, function, as well as CN version).

From Clark, "Ideally, we'd like a sample of whatever you've been focusing on in the past month." Please do not send duplicate examples month over month.

[bcpierce00]

I would suggest not spending any time initially trying to set up CI magic to do this automatically -- this actually seems quite hard (because they want a smallish number of queries that are diverse, novel, etc.).

[thatplguy]

I would suggest not spending any time initially trying to set up CI magic to do this automatically -- this actually seems quite hard (because they want a smallish number of queries that are diverse, novel, etc.).

Agreed. But it would be nice to automatically extract the identifying metadata if we're planning to do 100+ examples every month. Hopefully this won't be too hard.

[bcpierce00]

Maybe the identifying metadata can be included automatically by CN as comments at the top of SMTLib queries that it generates?

…

On Tue, Jul 16, 2024 at 11:44 AM Cole Schlesinger ***@***.***> wrote: I would suggest *not* spending any time initially trying to set up CI magic to do this automatically -- this actually seems quite hard (because they want a smallish number of queries that are diverse, novel, etc.). Agreed. But it would be nice to automatically extract the identifying metadata if we're planning to do 100+ examples every month. Hopefully this won't be too hard. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/GaloisInc/VERSE-Toolchain/issues/108*issuecomment-2231268233__;Iw!!IBzWLUs!Q9XmPXQyV4RxaoLIv0O9f8Ez0vzXiF7sIZolchBx-YrtHyU3BVLZ4EP7O1MVSw43XJlS4kK0u6xx5CxMfPTdg4xiY70P$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC6QBRWZPMECU47KM4TZMU5VNAVCNFSM6AAAAABK62GXZ2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEMZRGI3DQMRTGM__;!!IBzWLUs!Q9XmPXQyV4RxaoLIv0O9f8Ez0vzXiF7sIZolchBx-YrtHyU3BVLZ4EP7O1MVSw43XJlS4kK0u6xx5CxMfPTdg-2k3zqD$> . You are receiving this because you commented.Message ID: ***@***.***>