# Using coqnative compiled files in other files

**URL:** <https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122>\
**Category:** Using Rocq\
**Created:** [December 10, 2023, 8:37pm UTC](https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122 "2023-12-10T20:37:50Z")\
**Posts on this page:** 10\
**Page:** 1

<div class="post-metadata">

**Author:** ![chluebi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/chluebi/32/914_2.png) [@chluebi](https://discourse.rocq-prover.org/u/chluebi)\
**Post date:** [December 10, 2023, 8:37pm UTC](https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122/1 "2023-12-10T20:37:50Z")

</div>

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:

```bash
$ 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

```auto
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

```auto
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:

```auto
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?

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [December 10, 2023, 8:44pm UTC](https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122/2 "2023-12-10T20:44:10Z")

</div>

> 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.

---

<div class="post-metadata">

**Author:** ![chluebi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/chluebi/32/914_2.png) [@chluebi](https://discourse.rocq-prover.org/u/chluebi)\
**Post date:** [December 10, 2023, 8:45pm UTC](https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122/3 "2023-12-10T20:45:35Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [December 10, 2023, 10:13pm UTC](https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122/4 "2023-12-10T22:13:36Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [December 10, 2023, 10:15pm UTC](https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122/5 "2023-12-10T22:15:02Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [December 11, 2023, 8:10am UTC](https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122/6 "2023-12-11T08:10:23Z")

</div>

> [@chluebi](#):
>
> could you illustrate when native\_compute actually gives a speedup in a project then?

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.

```coq
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) *)

```

---

<div class="post-metadata">

**Author:** ![chluebi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/chluebi/32/914_2.png) [@chluebi](https://discourse.rocq-prover.org/u/chluebi)\
**Post date:** [December 11, 2023, 9:18am UTC](https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122/7 "2023-12-11T09:18:01Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![chluebi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/chluebi/32/914_2.png) [@chluebi](https://discourse.rocq-prover.org/u/chluebi)\
**Post date:** [December 11, 2023, 10:01am UTC](https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122/8 "2023-12-11T10:01:29Z")

</div>

Researching further now, I stumbled unto this: [ceps/text/048-packaging-coq-native.md at master · coq/ceps · GitHub](https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md)

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.

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [December 11, 2023, 10:03am UTC](https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122/9 "2023-12-11T10:03:28Z")

</div>

coqnative is unrelated to being configured with native enabled.

---

<div class="post-metadata">

**Author:** ![chluebi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/chluebi/32/914_2.png) [@chluebi](https://discourse.rocq-prover.org/u/chluebi)\
**Post date:** [December 11, 2023, 9:35pm UTC](https://discourse.rocq-prover.org/t/using-coqnative-compiled-files-in-other-files/2122/10 "2023-12-11T21:35:35Z")

</div>

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.