Something went wrong. Try again.
This repository has no description
Something went wrong. Try again.
1.1 kB · 25 lines
at main
1234567891011121314151617181920212223242526From PackageCalculus Require Import Prelude Core Versions Conflict Visibility Debian DebianMA Opam Cargo Alpine Npm Placement Smoke.From Stdlib Require Import Extraction ExtrOcamlBasic.
Extraction Language OCaml.
(* dune's coq.extraction runs coqc inside _build/default/extraction; the implicit output directory is the intended one. *)Set Extraction Output Directory ".".
(* The nat-instantiated smoke modules reach stdlib Type-valued parity constants (Nat.EvenT/OddT) that are Qed-opaque; extraction opens them, which is sound here because the reduction products are audited Closed under the global context (scripts/check-axioms.sh). *)Set Warnings "-extraction-opaque-accessed".
(* lex is a function, so OCaml's strictness evaluates both legs of every lexicographic comparison even when the first decides; inlining restores the short circuit. *)Extraction Inline lex.
Extraction "pac_extraction.ml" Smoke.C Smoke.Ver Smoke.Cfl Smoke.Conc Smoke.Peer Smoke.Vis Smoke.Feat Smoke.Virt Smoke.PkgF Smoke.VarF Smoke.FC Smoke.Op Smoke.Cgo Smoke.Alp Debian DebianMA Opam Cargo Alpine Npm Placement.