Using coqnative compiled files in other files

Using Coq
1

I was planning on running some tests on native_compute and as such I was trying to get native compilation to work.

  1. How do I use theorems generated .cmx (or is it .cmxs) files generated by coqnative in my normal proofchecking needs, i.e. use the theorems in a normal .v proof in coqide
  2. How do I compile to .cmx without needing to have the file proofchecked with native_compute disabled?

Version used:

$ coqc --version
The Coq Proof Assistant, version 8.18.0
compiled with OCaml 4.14.1

(Installed via nix)

Details:

Given the following Test.v

Theorem calc_native : 2110 + 2 = 2112.
Proof.
  native_compute.
  reflexivity.
Qed.

As far as I understand since 8.14 the way to compile this is seperate compilation, meaning I first have to compile this Test.v into a .vo file as follows:
coqc -R theories MyPackage ./theories/Test.v
Related to question 2:
This now runs the proofchecker with native_compute disabled (so it uses vm_compute instead) on my file, if this fails, I cannot compile to native, I do not want this but I could not find a way to skip the checking in the manual

Continuing:

Which together with other files also gives me
./theories/Test.vo
Now I can run
coqnative -R theories MyPackage ./theories/Test.vo
This generates
./theories/.coq-native/NTest.cmx
Now I want to use the calc_native inside of NTest.cmx in a new file

Test2.v

From MyPackage Require Import Test.

Theorem calc_native2 : 2110 + 2 = 2112.
Proof.
  apply calc_native.
Qed.

But if I delete the .vo file (because I don’t want to depend on it), and then try to compile Test2.v
coqc -R theories MyPackage ./theories/Test2.v
Gives error:

File "./theories/Test.v", line 1, characters 0-20:
Error: Cannot find a physical path bound to logical path Test.

This leads to question 1: How do I tell coqc or whatever coq program im using to use the .cmx file generated by coqnative?

2

But if I delete the .vo file (because I don’t want to depend on it), and then try to compile Test2.v

You have a misunderstanding about what native compilation does. It only provides the native_compute reduction and checking conversions using it (native cast <<:). You still need the .vo.

3

I see, could you illustrate when native_compute actually gives a speedup in a project then? Basically I want to see when native_compute actually gets run as itself instead of replaced by vm_compute.

Note: not sure if I properly replied to you, the thread layout is a bit confusing

4

native_compute should run as itself and not be replaced by vm_compute if Coq was compile-time configured for it.
When installing coq through opam this is done by installing the coq-native packages.

1 Like
5

If you actually see a speedup depends on what you’re computing. I’m not familiar enough with native_compute to say more than that.

6

Let us suppose that a native_compute proof check runs 5x faster than a vm_compute one, but that it suffers from a startup penalty of 1 second. (Your mileage may vary.) Therefore, on a 1s proof, you will experience a slowdown when switching from vm_compute to native_compute. On a 2s proof, you will experience a speedup, but nothing dramatic. On a 5s proof, things start to get interesting, because you will shave 3s from the proof checking.

Here is a toy example using a proper definite integral that is known to be computationally intensive. The same proof is performed twice, first with vm_compute, second with native_compute. (The respective calls are hidden behind the integral tactic.) Here, the native_compute proof is checked about five time faster.

From Coq Require Import Reals.
From Coquelicot Require Import Coquelicot.
From Interval Require Import Tactic.
Open Scope R_scope.
Notation "x = y ± z" := (Rle (Rabs (x - y)) z) (at level 70, y at next level).

Goal RInt (fun x => sin (x + exp x)) 0 8 = 0.34740017 ± 1e-8.
Proof. Time integral with (i_fuel 10000). Qed.
(* Finished transaction in 10.018 secs (10.015u,0.003s) *)

Goal RInt (fun x => sin (x + exp x)) 0 8 = 0.34740017 ± 1e-8.
Proof. Time integral with (i_fuel 10000, i_native_compute). Qed.
(* Finished transaction in 1.976 secs (1.869u,0.s) *)
1 Like
7

Thank you very much for the example!

I seem to be having troubles with actually getting the second proof to use native computation as it just falls back to vm_compute.

Running something like
coqtop -R theories MyPackage < ./theories/Test.v
Tells me that the native compiler is disabled

But passing the deprecated -native-compiler yes flag is ignored.

I did run coqnative on the file beforehand, but it seems to me like coqtop is not using it.

8

Researching further now, I stumbled unto this: ceps/text/048-packaging-coq-native.md at master · coq/ceps · GitHub

This to me seems to suggest that I cannot use native_compute unless all dependencies are also natively compiled etc. which is normally done with the opam coq-native package which just sets a flag for when coq is installed via opam.

As the default coq nixpkgs installation does not do that, I cannot use native_compute?

I suppose then the course of action is either to switch over to opam or make my own coq nix derivation.

This would follow what @SkySkimmer said, but im not sure if this is now already outdated because coqnative exists.

9

coqnative is unrelated to being configured with native enabled.

1 Like
10

For if anyone cares, I’ve spent a few hours trying to get it to work with the default.nix file in the coq repository and didn’t really get anywhere, so if anyone is in the same situation as me, I would reccomend just using opam instead.