Is anyone else slightly interested in this? I mostly have questions about implementation decisions (taking into consideration that I know very little about the subject :/)
I can discuss it with you. (Not for long, I am teaching this afternoon, and saying I am ready would be quite the overstatement.)
Great! So should we go to a breakout room?
I think I will join as well for now...
(we're in breakout room 3)
We'll reconvene tomorrow at 10:00 UTC+1
This recently came up in our (@Jakob Botsch Nielsen 's) work on extraction to rust. Int32 would be useful.
So, as it happens, compiling a 32-bit Coq is not that complicated. I first did
apt-get install gcc-multilib libgmp-dev:i386 (so, Debian/Ubuntu setup), and then ran
opam switch create 4.11.1+32bit. @Ana de Almeida Borges @Maxime Dénès @Pierre Roux
Indeed we maintain a recipe for the 32bit compilation on our CI, that's more or less the canonical reference
For anyone interested, we decided to meet again tomorrow at 10:00 UTC+1.
Nice to know. Last time, I relied on a VM, that was much more painful.
I have pushed the changes we have been doing here: https://github.com/ana-borges/coq/tree/primitive_integers
We meet again tomorrow (Thursday) at 10:00 UTC+1
Today Pierre and I finished the printing and parsing. I should still test it more thoroughly, but it's looking good for now! Here is a draft PR: https://github.com/coq/coq/pull/13559
I will try to work on the missing things on my own, but I would like more heads thinking about the division issue. @Guillaume Melquiond will you be available for half an hour at some point this week?
I am done teaching at 6pm (utc+1). Otherwise tomorrow any time after 2:30pm.
As you wish. I am free either time. You can ping me here and I'll probably see it +/- immediately.
@Pierre Roux I think we did something wrong during the rebase yesterday... I am trying to fix it, but I still don't fully understand the printing / parsing, so I would be glad if you could take a look :)
I guess some renaming from
Primint63.int is needed since the primitive type moved. There could be such occurences in
plugin/syntax/number.ml. And probably the same for
That's what I thought, yes. I'm currently looking for them
I can't find more things to change, but I still get the same error... I think
locate_int63 is returning
None instead of
Some ..., but I don't understand why
I am available to discuss. @Ana de Almeida Borges
:) BBB room 1?
I would be interested in a recap on what has been achieved / is still open. How about a quick info in the daily wrap up today?
Last updated: Jun 11 2023 at 00:30 UTC