Adding FStar.Printable.fst with test by proof in tests/printable usin…

[briangmilnes]

No description provided.

[mtzguido]

Hi Brian, thanks! It mostly looks good, I just have one comment. There's no need to make this tests/printable directory, nor check F*'s output. Just putting this test file in, say, tests/micro-benchmarks is enough to get into the existing rules which will check that everything succeeds.

Could you make that change? Simply pushing to your branch will update the PR accordingly.

[briangmilnes]

Sure, but I've been hacking a clean FStarUnit testing framework, in which I would add the one test that does not run in normalization. If some of you folks look at it and like it. Otherwise, I'll just do it the easy way.

…

On Sun, Apr 30, 2023 at 8:19 PM Guido Martínez ***@***.***> wrote: Hi Brian, thanks! It mostly looks good, I just have one comment. There's no need to make this tests/printable directory, nor check F*'s output. Just putting this test file in, say, tests/micro-benchmarks is enough to get into the existing rules which will check that everything succeeds. Could you make that change? Simply pushing to your branch will update the PR accordingly. — Reply to this email directly, view it on GitHub <#2902 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACKMDK33D4WQOEXTS5TMZUDXD4TTDANCNFSM6AAAAAAXRLRN5U> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[mtzguido]

Ah, I see. Could we anyway make that a separate PR, and not block this one on the unit testing stuff?

[briangmilnes]

No problem. Likely tomorrow. I'll do a pull and the merge first, as per some CONTRIBUTING doc I found.

…

-B

On Mon, May 1, 2023 at 9:35 AM Guido Martínez ***@***.***> wrote: Ah, I see. Could we anyway make that a separate PR, and not block this one on the unit testing stuff? — Reply to this email directly, view it on GitHub <#2902 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACKMDK3ZIAWHL7BR3J62JZDXD7Q5DANCNFSM6AAAAAAXRLRN5U> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[briangmilnes]

Guido, TestPrintable moved to micro-benchmarks. All tests completed.

[mtzguido]

Hi Brian, I see you've merged master, but I don't see any other changes. Did you maybe forget to push?

[briangmilnes]

Darn it, I did push. Just did it again too. I pushed to the master not my branch it appears. Do you know the fix? Now a push to my branch is rejected. Give me a few unless you know the recipe.

…

On Mon, May 1, 2023 at 2:59 PM Guido Martínez ***@***.***> wrote: Hi Brian, I see you've merged master, but I don't see any other changes. Did you maybe forget to push? — Reply to this email directly, view it on GitHub <#2902 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACKMDKZGHJUWW2IPUVCWCJDXEAW3FANCNFSM6AAAAAAXRLRN5U> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[mtzguido]

I see it now! Just please also remove the change to tests/Makefile

[briangmilnes]

Done, the printable branch looks good with makefile change done.

…

On Mon, May 1, 2023 at 3:18 PM Guido Martínez ***@***.***> wrote: I see it now! Just please also remove the change to tests/Makefile — Reply to this email directly, view it on GitHub <#2902 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACKMDK3WWVJ36JKZKSYBAVTXEAZEVANCNFSM6AAAAAAXRLRN5U> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[mtzguido]

Thanks Brian, just merged this.