Skip to content

Navigation Menu

Appearance settings

- AI CODE CREATION
  GitHub CopilotWrite better code with AI
  GitHub Copilot appDirect agents from issue to merge
  MCP Registry^NewIntegrate external tools
- DEVELOPER WORKFLOWS
  ActionsAutomate any workflow
  CodespacesInstant dev environments
  IssuesPlan and track work
  Code ReviewManage code changes
- APPLICATION SECURITY
  GitHub Advanced SecurityFind and fix vulnerabilities
  Code securitySecure your code as you build
  Secret protectionStop leaks before they start
- EXPLORE
  Why GitHub
  Documentation
  Blog
  Changelog
  Marketplace
View all features
- BY COMPANY SIZE
  Enterprises
  Small and medium teams
  Startups
  Nonprofits
- BY USE CASE
  App Modernization
  DevSecOps
  DevOps
  CI/CD
  View all use cases
- BY INDUSTRY
  Healthcare
  Financial services
  Manufacturing
  Government
  View all industries
View all solutions
- EXPLORE BY TOPIC
  AI
  Software Development
  DevOps
  Security
  View all topics
- EXPLORE BY TYPE
  Customer stories
  Events & webinars
  Ebooks & reports
  Business insights
  GitHub Skills
- SUPPORT & SERVICES
  Documentation
  Customer support
  Community forum
  Trust center
  Partners
View all resources
- COMMUNITY
  GitHub SponsorsFund open source developers
- PROGRAMS
  Security Lab
  Maintainer Community
  Accelerator
  GitHub Stars
  Archive Program
- REPOSITORIES
  Topics
  Trending
  Collections
- ENTERPRISE SOLUTIONS
  Enterprise platformAI-powered developer platform
- AVAILABLE ADD-ONS
  GitHub Advanced SecurityEnterprise-grade security features
  Copilot for BusinessEnterprise-grade AI features
  Premium SupportEnterprise-grade 24/7 support
Pricing

Search code, repositories, users, issues, pull requests...

Search

Clear

Search syntax tips

Provide feedback

We read every piece of feedback, and take your input very seriously.

Include my email address so I can be contacted

Saved searches

Use saved searches to filter your results more quickly

Name

Query

To see all available qualifiers, see our documentation.

Appearance settings

You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session.

Dismiss alert

rocq-prover / rocq Public

Notifications You must be signed in to change notification settings
Fork 736
Star 5.5k

Code
Issues 2.5k
Pull requests 76
Actions
Projects
Wiki
Security and quality
Insights

Additional navigation options

Code
Issues
Pull requests
Actions
Projects
Wiki
Security and quality
Insights

made native compilation compile to malfunction#22136

Draft

IBBXEF wants to merge 76 commits into

rocq-prover:masterrocq-prover/rocq:masterfrom

IBBXEF:masterIBBXEF/rocq-native-mlf:masterCopy head branch name to clipboard

Conversation Commits76 (76)Checks Files changed

Draft

made native compilation compile to malfunction#22136
IBBXEF wants to merge 76 commits into
rocq-prover:masterfrom
IBBXEF:master

Commits

Commits on Jun 19, 2026

enabling native-compiler
IBBXEF
committed
Created placeholder functions for compiling to mlf
IBBXEF
committed
Is now able to compile strings, floats and sequences of mllambda to malfunction
IBBXEF
committed
the generated mlf code is now syntaxically correct
IBBXEF
committed
Now compiles lambda functions
IBBXEF
committed
Now compiles primitives
IBBXEF
committed
the mlf compiler is now called by the general compile function
IBBXEF
committed
fixed two naming errors
IBBXEF
committed
Now compiles local and global variable names, applications and let statements
IBBXEF
committed
Now compiles if and letrec statements, and fixed a bug with global names
IBBXEF
committed
Now compiles (at least define) let cases
IBBXEF
committed
Now compiles global table fix types (whatever that is)
IBBXEF
committed
Now compiles global table norm and fixed a few bugs
IBBXEF
committed
Fixed a capitalization error and a few inconsistencies
IBBXEF
committed
Now compiles arrays and reference assignment
IBBXEF
committed
Fixed an arror where global names where wrongly assumed to come from the same file
IBBXEF
committed
Fixed a bug introduced by the last fix where some global variable would have two dolla sign in front of them
IBBXEF
committed
refactored some of the code and fixed a bug where () would be translated as $() instead of 0
IBBXEF
committed
rt1 and rt2 are now correctly marked as coming from the Nativelib module
IBBXEF
committed
refactored pp_gname_plf
IBBXEF
committed
Fixed an error whith double dollar signs before variables
IBBXEF
committed
Now compiles match statements
IBBXEF
committed
Now compiles primitives Mk_fix and Mk_var
IBBXEF
committed
Fixed a double dollar bug and some values being wrongly compiled as functions
IBBXEF
committed
Fixed multiple cases where definition would be compiled as functions, and string_of_gname_mlf now properly handles wildcards
IBBXEF
committed
Now compiles global cofix tables and all global declaration !
IBBXEF
committed
Now compiles MLconstruct and MLisaccu, and thus, all mllambda expressions ! also refactored many functions.
IBBXEF
committed
Now compiles lazy values correctly
IBBXEF
committed
Started to make a function to call the mlf compiler
IBBXEF
committed
Now correctly compiles uints and floats in 32 and 64 bits architectures
IBBXEF
committed
Now correctly compiles negative ints
IBBXEF
committed
Refactored code and improved generated code identation
IBBXEF
committed
fixed bugs with uint compilation, refactored code, removed useless parentheses and improved identation of the generated code
IBBXEF
committed
refactored and fixed typos
IBBXEF
committed
Now compiles field access correctly
IBBXEF
committed
the malfunction compiler is now called
IBBXEF
committed
letrec are now compiled properly
IBBXEF
committed
imports from generated ml file now imports from the equivalent mlf file
IBBXEF
committed
writing a mlf program now also generate a .mli file specifying its interface
IBBXEF
committed
The mlf compilation now works
IBBXEF
committed
Cleaned code and did a small fix
IBBXEF
committed
ML primitives without arguments are now correctly compiled as values and not function applications
IBBXEF
committed
Compilation now works perfectly
IBBXEF
committed
Cleaned generated code and fixed ml primitives being imported from the wrong module
IBBXEF
committed
Fixed Lazy.force being incorrectly compiled
IBBXEF
committed
Fixed an error in string compilation
IBBXEF
committed
Generated interface is now compatible with Ocaml native compilation
IBBXEF
committed
.mli interfaces now contains defined types
IBBXEF
committed
refactored code, and generated interfaces now have types more coherent with inner value
IBBXEF
committed
Now correctly compiles floats, Array.get and cofix
IBBXEF
committed
Now correctly compiles cofix
IBBXEF
committed
removed now unecessary code
IBBXEF
committed
Now correctly handles nan and infinity
IBBXEF
committed
Now handles decode_string and compilation in specific folders
IBBXEF
committed
Went back to simpler mli generation as interfacing with Ocaml will no longer be needed
IBBXEF
committed
removed Ocaml compilation
IBBXEF
committed
Added cleaner debug messages and error handling
IBBXEF
committed
removed most of Ocaml code generation
IBBXEF
committed
More cleanup, reused now free function names, and moved Lazy.force into a MLprimitive
IBBXEF
committed
more renaming
IBBXEF
committed
fixed identation
IBBXEF
committed
pp_lname now adds truly returns the variable name in mlf (with the dollar)
IBBXEF
committed
replaced arrays with normal memory blocks
IBBXEF
committed
removed Obj_magic primitive as it is no longer needed
IBBXEF
committed
The compilation of logical and is now cleaner
IBBXEF
committed
fixed a comment
IBBXEF
committed
removed some support for the creation of clotures on primitives
IBBXEF
committed
added a space to make code generation clearer
IBBXEF
committed
added a MLmatch_noaccu contructor to mllambda
IBBXEF
committed
removed annotations from matches as they are no longer needed
IBBXEF
committed
removed annotations from Gletcase as they are no longer needed
IBBXEF
committed
vendor malfunction
IBBXEF
committed
updated docker files
IBBXEF
committed
removed malfunction vendor
IBBXEF
committed
updated Dockerfile
IBBXEF
committed
The compilation of Uint, float, and pstring into mlf is now separated in a different function to stay compatible with extraction
IBBXEF
committed

Footer

© 2026 GitHub, Inc.

Footer navigation

Terms
Privacy
Security
Status
Community
Docs
Contact

You can’t perform that action at this time.