made native compilation compile to malfunction by IBBXEF · Pull Request #22136 · rocq-prover/rocq

IBBXEF · 2026-06-17T12:21:44Z

No description provided.

coqbot-app · 2026-06-17T12:21:47Z

Hello, thanks for your pull request!
In the future, we strongly recommend that you do not use master as the name of your branch when submitting a pull request.
By the way, you may be interested in reading our contributing guide.

coqbot-app · 2026-06-17T12:21:48Z

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

SkySkimmer · 2026-06-17T12:22:15Z

@coqbot run full ci

coqbot-app · 2026-06-17T13:11:40Z

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

coqbot-app · 2026-06-17T13:17:36Z

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

SkySkimmer · 2026-06-17T13:20:02Z

@coqbot run full ci

coqbot-app · 2026-06-17T13:32:29Z

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

coqbot-app · 2026-06-17T13:36:53Z

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

coqbot-app · 2026-06-17T13:41:37Z

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

SkySkimmer · 2026-06-17T13:42:18Z

@coqbot run full ci

SkySkimmer · 2026-06-17T15:14:12Z

-let compile f =
-  Printf.sprintf "Float64.of_float (%s)" (to_hex_string f)
+(* Compiles a float to malfunction code *)
+let compile f = (* malfunction does not support writing -1.1, so we have to be careful *)


it seems this function is also used by extraction, so instead of modifying it you should add a new compile_malfunction or some such thing

same for pstring

Ok, I fixed it !

SkySkimmer · 2026-06-17T15:19:17Z

not sure what's going on with 32bit
stdlib_test and metarocq are failing because of the "compile" functions used by extraction, cf my previous comments
mathcomp gets a stack overflow in malfunction, IDK if mathcomp is expected to work with native compile though (mathcomp_test disables it but mathcomp itself keeps it enabled)

…alfunction

… longer be needed

SkySkimmer · 2026-06-19T11:10:01Z

can't rerun CI until you rebase

…to a MLprimitive

…llar)

… in a different function to stay compatible with extraction

coqbot-app · 2026-06-19T11:13:46Z

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

IBBXEF · 2026-06-19T11:16:14Z

I rebased my branch

SkySkimmer · 2026-06-19T11:20:22Z

@coqbot run full ci

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 17, 2026

coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 17, 2026

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 17, 2026

coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 17, 2026

IBBXEF force-pushed the master branch from dd91c9e to 95b280b Compare June 17, 2026 13:32

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 17, 2026

IBBXEF force-pushed the master branch from 95b280b to 99792ab Compare June 17, 2026 13:36

IBBXEF force-pushed the master branch from 99792ab to f009fa8 Compare June 17, 2026 13:41

coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 17, 2026

SkySkimmer reviewed Jun 17, 2026

View reviewed changes

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 18, 2026

IBBXEF added 8 commits June 19, 2026 13:09

enabling native-compiler

b9d8ed6

Created placeholder functions for compiling to mlf

33e6df3

Is now able to compile strings, floats and sequences of mllambda to m…

a8e57bd

…alfunction

the generated mlf code is now syntaxically correct

94ae065

Now compiles lambda functions

cb7f597

Now compiles primitives

032618d

the mlf compiler is now called by the general compile function

90d59b1

fixed two naming errors

cb50f17

IBBXEF added 3 commits June 19, 2026 13:09

Went back to simpler mli generation as interfacing with Ocaml will no…

c731fa3

… longer be needed

removed Ocaml compilation

fb1135e

Added cleaner debug messages and error handling

20f7b06

IBBXEF added 19 commits June 19, 2026 13:11

removed most of Ocaml code generation

5da2bc1

More cleanup, reused now free function names, and moved Lazy.force in…

69ba091

…to a MLprimitive

more renaming

6e46e62

fixed identation

f0f9fbd

pp_lname now adds truly returns the variable name in mlf (with the do…

4f54bc5

…llar)

replaced arrays with normal memory blocks

456c5d5

removed Obj_magic primitive as it is no longer needed

46f7191

The compilation of logical and is now cleaner

490074a

fixed a comment

2fc7811

removed some support for the creation of clotures on primitives

6863127

added a space to make code generation clearer

958a006

added a MLmatch_noaccu contructor to mllambda

f5bd314

removed annotations from matches as they are no longer needed

9ddba0a

removed annotations from Gletcase as they are no longer needed

b293a83

vendor malfunction

580cd79

updated docker files

6f83b24

removed malfunction vendor

11b4496

updated Dockerfile

0a54420

The compilation of Uint, float, and pstring into mlf is now separated…

2a56529

… in a different function to stay compatible with extraction

IBBXEF force-pushed the master branch from 0361de4 to 2a56529 Compare June 19, 2026 11:13

coqbot-app Bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Jun 19, 2026

coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 19, 2026

Conversation

IBBXEF commented Jun 17, 2026

Uh oh!

coqbot-app Bot commented Jun 17, 2026

Uh oh!

coqbot-app Bot commented Jun 17, 2026

Uh oh!

SkySkimmer commented Jun 17, 2026

Uh oh!

coqbot-app Bot commented Jun 17, 2026

Uh oh!

coqbot-app Bot commented Jun 17, 2026

Uh oh!

SkySkimmer commented Jun 17, 2026

Uh oh!

coqbot-app Bot commented Jun 17, 2026

Uh oh!

coqbot-app Bot commented Jun 17, 2026

Uh oh!

coqbot-app Bot commented Jun 17, 2026

Uh oh!

SkySkimmer commented Jun 17, 2026

Uh oh!

SkySkimmer Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

SkySkimmer Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

SkySkimmer Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

IBBXEF Jun 19, 2026

Choose a reason for hiding this comment

Uh oh!

SkySkimmer commented Jun 17, 2026

Uh oh!

SkySkimmer commented Jun 19, 2026

Uh oh!

coqbot-app Bot commented Jun 19, 2026

Uh oh!

IBBXEF commented Jun 19, 2026

Uh oh!

SkySkimmer commented Jun 19, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants