Ana de Almeida Borges (Nov 30 2020 at 09:53): Ana de Almeida Borges (Nov 30 2020 at 09:53):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 :/)
Guillaume Melquiond (Nov 30 2020 at 09:54):I can discuss it with you. (Not for long, I am teaching this afternoon, and saying I am ready would be quite the overstatement.)
Ana de Almeida Borges (Nov 30 2020 at 09:55):Great! So should we go to a breakout room?
Cyril Cohen (Nov 30 2020 at 09:55):I think I will join as well for now...
Ana de Almeida Borges (Nov 30 2020 at 09:59):(we're in breakout room 3)
Ana de Almeida Borges (Nov 30 2020 at 11:28):We'll reconvene tomorrow at 10:00 UTC+1
Bas Spitters (Nov 30 2020 at 12:23):This recently came up in our (@Jakob Botsch Nielsen 's) work on extraction to rust. Int32 would be useful.
Guillaume Melquiond (Dec 01 2020 at 17:06):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
Emilio Jesús Gallego Arias (Dec 01 2020 at 17:33):Indeed we maintain a recipe for the 32bit compilation on our CI, that's more or less the canonical reference
Ana de Almeida Borges (Dec 01 2020 at 17:44):Great!
For anyone interested, we decided to meet again tomorrow at 10:00 UTC+1.
Pierre Roux (Dec 01 2020 at 18:25):Nice to know. Last time, I relied on a VM, that was much more painful.
Ana de Almeida Borges (Dec 01 2020 at 19:31):I have pushed the changes we have been doing here: https://github.com/ana-borges/coq/tree/primitive_integers
Ana de Almeida Borges (Dec 02 2020 at 23:01):We meet again tomorrow (Thursday) at 10:00 UTC+1
Ana de Almeida Borges (Dec 03 2020 at 11:31):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
Ana de Almeida Borges (Dec 03 2020 at 11:33):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?
Guillaume Melquiond (Dec 03 2020 at 12:22):I am done teaching at 6pm (utc+1). Otherwise tomorrow any time after 2:30pm.
Ana de Almeida Borges (Dec 03 2020 at 15:21):As you wish. I am free either time. You can ping me here and I'll probably see it +/- immediately.
Ana de Almeida Borges (Dec 04 2020 at 11:43):@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 :)
Pierre Roux (Dec 04 2020 at 12:04):I guess some renaming from Int63.int to Primint63.int is needed since the primitive type moved. There could be such occurences in PrimInt63.v, SInt63.v and plugin/syntax/number.ml. And probably the same for int_wrapper.
Ana de Almeida Borges (Dec 04 2020 at 12:05):That's what I thought, yes. I'm currently looking for them
Ana de Almeida Borges (Dec 04 2020 at 12:34):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
Guillaume Melquiond (Dec 04 2020 at 13:15):I am available to discuss. @Ana de Almeida Borges
Ana de Almeida Borges (Dec 04 2020 at 13:17)::) BBB room 1?
Michael Soegtrop (Dec 04 2020 at 15:48):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