maximedenes / native-coq Goto Github PK
View Code? Open in Web Editor NEWCoq with native compilation, as well as machine integers and arrays !
License: GNU Lesser General Public License v2.1
Coq with native compilation, as well as machine integers and arrays !
License: GNU Lesser General Public License v2.1
THE COQ V8 SYSTEM ================= INSTALLATION. ============= See the file INSTALL for installation procedure. DOCUMENTATION. ============== The documentation is part of the archive in directory doc. The documentation of the last released version is available on the Coq web site at http://coq.inria.fr/doc. CHANGES. ======== There is a file named CHANGES that explains the differences and the incompatibilities since last versions. If you upgrade Coq, please read it carefully. AVAILABILITY. ============= Coq is available at http://coq.inria.fr, or, for older versions at ftp://ftp.inria.fr/INRIA/LogiCal/coq. THE COQ CLUB. ============= The Coq Club moderated mailing list is meant to be a standard way to discuss questions about the Coq system and related topics. The submission address is: [email protected] The topics to be discussed in the club should include: * technical problems; * questions about proof developments; * suggestions and questions about the implementation; * announcements of proofs; * theoretical questions about typed lambda-calculi which are closely related to Coq. To be added to, or removed from, the mailing list, please write to: [email protected] Please use also this address for any questions/suggestions about the Coq Club. It might sometimes take a few days before your messages get forwarded. BUGS REPORT. ============ Send your bug reports by filling a form at http://coq.inria.fr/bugs To be effective, bug reports should mention the Caml version used to compile and run Coq, the Coq version (coqtop -v), the configuration used, and include a complete source example leading to the bug.
Coq supports a larger subset of Unicode inidentifiers than OCaml, so we're sometimes producing incorrect OCaml code. Extraction would probably provide us the appropriate machinery.
Values defined at toplevel should be evaluated in a lazy fashion:
Definition n := fact 100.
Eval native_compute in true.
Should answer instantly "true".
For now each call to native_compute adds a module import in subsequent calls.
An import is actually needed only if part of the environment was on the compilation stack before the call.
Definition b := true.
Write State "foo_state".
Restore State "foo_state".
cannot find file /home/mdenes/native-coq/kernel/foo_state.coq.cmxs in search path
Eval native_compute in b.
Compilation...
File "/tmp/Coq_native6784ac.ml", line 6, characters 2-14:
Error: Unbound value const_NTop_b
Anomaly: Compilation failure. Please report.
Definition foo := true.
Definition bar := foo.
Eval native_compute in bar.
is compiled to:
let const_Ntest_interactive_foo =
(Obj.magic (NCoq_Init_Datatypes.Construct_NCoq_Init_Datatypes_bool_0_0) : Nativevalues.t)
let const_Ntest_interactive_bar =
Coq_native1cf0e1.const_Ntest_interactive_foo
Line 952 in cb563dd
When extracting to ocaml, native ints are extracted to Uint63.t.
However, file native-coq/theories/Array/ExtractNative.v
still extracts constants using implementation native-coq/theories/Array/extrNative.ml
instead of native-coq/kernel/uint63.ml
.
In order to update ExtractNative.v
, we need to implement a few missing bits in uint63.ml
, like foldi_cont
, foldi_down_cont
, print_uint
and probably a few others.
If we want developments using native compilation to be compatible with regular makefiles, we should store the compiled code in vo files.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.