Get familiar with CN

[thatplguy]

Bonus: fix up/augment CN examples in the repo.

[bcpierce00]

There are examples in several places now -- the CN repo, the CN-tutorial repo, and I believe some in a private repo of Mike's. We should consolidate (maybe in the tutorial, for the moment at least?).

…

On Thu, Apr 11, 2024 at 12:04 AM Cole Schlesinger ***@***.***> wrote: Bonus: fix up/augment CN examples in the repo. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/GaloisInc/VERSE-Toolchain/issues/31__;!!IBzWLUs!TbsZ0GtA25bjWUj5oIFvRN4wkpwhI1ZiFNc-yQ0v7W8-PwPAQrigp87V1IgVhRn594YWVno4q1iN15Wi1J_2LoqFHMqT$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC3QCQXNJHDRIHVAXJDY4YDVXAVCNFSM6AAAAABGBR4K2SVHI2DSMVQWIX3LMV43ASLTON2WKOZSGIZTMOBWG43TCNA__;!!IBzWLUs!TbsZ0GtA25bjWUj5oIFvRN4wkpwhI1ZiFNc-yQ0v7W8-PwPAQrigp87V1IgVhRn594YWVno4q1iN15Wi1J_2LnvdWVGF$> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[thatplguy]

Good point @bcpierce00. There's another ticket for more rigorously creating examples – #3. I'll add pointers to the CN and CN-tutorial repos there. Happy to have the examples live in the tutorial.

[septract]

@bcpierce00 My old examples are now parked here. They should be merged into the tutorial repo I expect. I think @yav was fixing them so they pass the new syntax.

[bcpierce00]

Lots of good stuff here. In particular, I hope the linear and binary search can get ported to the tutorial soon.

…

On Tue, Apr 16, 2024 at 2:10 PM Mike Dodds ***@***.***> wrote: @bcpierce00 <https://urldefense.com/v3/__https://github.com/bcpierce00__;!!IBzWLUs!Vxo__k6mXGTjaalC3qTz74Sq3eoQGkC161Q6CPKdPUZZAV2v3-rbo9WrkIWN-93rG0kw48wko_bA5n9DC-hnSTxNLJ8W$> My old examples are now parked here <https://urldefense.com/v3/__https://github.com/GaloisInc/VERSE-Toolchain/tree/main/cn-intro__;!!IBzWLUs!Vxo__k6mXGTjaalC3qTz74Sq3eoQGkC161Q6CPKdPUZZAV2v3-rbo9WrkIWN-93rG0kw48wko_bA5n9DC-hnSVVzcsEG$>. They should be merged into the tutorial repo I expect. I think @yav <https://urldefense.com/v3/__https://github.com/yav__;!!IBzWLUs!Vxo__k6mXGTjaalC3qTz74Sq3eoQGkC161Q6CPKdPUZZAV2v3-rbo9WrkIWN-93rG0kw48wko_bA5n9DC-hnSQ8nYqgJ$> was fixing them so they pass the new syntax. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/GaloisInc/VERSE-Toolchain/issues/31*issuecomment-2059671132__;Iw!!IBzWLUs!Vxo__k6mXGTjaalC3qTz74Sq3eoQGkC161Q6CPKdPUZZAV2v3-rbo9WrkIWN-93rG0kw48wko_bA5n9DC-hnSUaGtl4L$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQCYXORSTEW2IKCFUTMLY5VSSXAVCNFSM6AAAAABGBR4K2SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDANJZGY3TCMJTGI__;!!IBzWLUs!Vxo__k6mXGTjaalC3qTz74Sq3eoQGkC161Q6CPKdPUZZAV2v3-rbo9WrkIWN-93rG0kw48wko_bA5n9DC-hnSVJLIwJA$> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[dc-mak]

@thatplguy wondering if this issue may be closed?

[bcpierce00]

Don't think the nice examples have been tutorialized yet...

…

On Fri, Jul 5, 2024 at 4:32 AM Dhruv Makwana ***@***.***> wrote: @thatplguy <https://urldefense.com/v3/__https://github.com/thatplguy__;!!IBzWLUs!SEY_KA8fEGLuPpRH6O2_RXLKGqyQA-1qJ9Z49KH-kZF-ZuRTdUVMKCBeeVvfnSAdPvrqmBhZThB4q-wJ61hhOryKGztF$> wondering if this issue be closed? — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/GaloisInc/VERSE-Toolchain/issues/31*issuecomment-2210440886__;Iw!!IBzWLUs!SEY_KA8fEGLuPpRH6O2_RXLKGqyQA-1qJ9Z49KH-kZF-ZuRTdUVMKCBeeVvfnSAdPvrqmBhZThB4q-wJ61hhOk3hoNRN$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC5PQKPYCRRNGPHTGKTZKZK3FAVCNFSM6AAAAABGBR4K2SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEMJQGQ2DAOBYGY__;!!IBzWLUs!SEY_KA8fEGLuPpRH6O2_RXLKGqyQA-1qJ9Z49KH-kZF-ZuRTdUVMKCBeeVvfnSAdPvrqmBhZThB4q-wJ61hhOltP8h7u$> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[podhrmic]

This issue should have been closed a long ago - we marked it as Done before the Github Project board automatically closed issues that are done (see this post)

[podhrmic]

Closing now for consistency, please reopen if you think it is not done (or perhaps open a new issue that is a bit more specific @bcpierce00 ?).

[septract]

I've captured the residual TODO here: rems-project/cn-tutorial#39