# Ocaml native int63 extraction

**URL:** https://discourse.rocq-prover.org/t/ocaml-native-int63-extraction/2065
**Category:** Using Rocq
**Created:** [October 3, 2023, 11:05am UTC](https://discourse.rocq-prover.org/t/ocaml-native-int63-extraction/2065 "2023-10-03T11:05:30Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![alx](https://avatars.discourse-cdn.com/v4/letter/a/59ef9b/32.png) [@alx](https://discourse.rocq-prover.org/u/alx)
#### Post date: [October 3, 2023, 11:05am UTC](https://discourse.rocq-prover.org/t/ocaml-native-int63-extraction/2065/1 "2023-10-03T11:05:30Z")

</div>

Hello everybody,

## I have a file Sample.v with the content

Require Import String.  
Require Import Int63.Sint63.  
Require Import PArray.  
Require Import Ascii String Coq.Strings.Byte.

Module Sample.

Definition bytes : Set := string.

Definition len\_bytes (s:bytes) := 1+ length s.

## End Sample.

and a file with the content

* * *

Require Export Sample.  
Require Extraction.  
Require ExtrOcamlBasic.  
Require ExtrOCamlInt63.  
Require ExtrOcamlChar.  
Require ExtrOcamlNativeString.

Extraction Language OCaml.

## Extraction Library Sample.

When I extract the Ocaml code I get

* * *

open Datatypes  
open Nat  
open String

module Sample =  
struct  
type bytes = string

(\*\* val to\_bytes : string → nat \*\*)

## let len\_bytes s = add (S O) (length s) end

And now my question comes. Where I can find the compiled code/library/interfaces  
for the modules Nat, Datatypes and String?  
Of course I can extract them and compile myself, but this triggers generation of  
other modules. This is actually good enough, but maybe there is some simpler  
way to compile my extracted sample (precompiled libraries or something). I have  
already spent a good deal of time looking for a solution, but I did not find one.

All the best,  
Alx