Stream: CUDW 2020

Topic: WG: primitive integers


view this post on Zulip 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 :/)

view this post on Zulip 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.)

view this post on Zulip Ana de Almeida Borges (Nov 30 2020 at 09:55):

Great! So should we go to a breakout room?

view this post on Zulip Cyril Cohen (Nov 30 2020 at 09:55):

I think I will join as well for now...

view this post on Zulip Ana de Almeida Borges (Nov 30 2020 at 09:59):

(we're in breakout room 3)

view this post on Zulip Ana de Almeida Borges (Nov 30 2020 at 11:28):

We'll reconvene tomorrow at 10:00 UTC+1

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre Roux (Dec 01 2020 at 18:25):

Nice to know. Last time, I relied on a VM, that was much more painful.

view this post on Zulip 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

view this post on Zulip Ana de Almeida Borges (Dec 02 2020 at 23:01):

We meet again tomorrow (Thursday) at 10:00 UTC+1

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Guillaume Melquiond (Dec 03 2020 at 12:22):

I am done teaching at 6pm (utc+1). Otherwise tomorrow any time after 2:30pm.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Dec 04 2020 at 12:05):

That's what I thought, yes. I'm currently looking for them

view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Dec 04 2020 at 13:15):

I am available to discuss. @Ana de Almeida Borges

view this post on Zulip Ana de Almeida Borges (Dec 04 2020 at 13:17):

:) BBB room 1?

view this post on Zulip 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: Oct 16 2021 at 09:07 UTC