Documentazione di lungo

Il tuo primo pacchetto TypeScript costruito da Lean

Scrivi definizioni Lean e una dimostrazione, genera con lungo un pacchetto npm eseguito su WebAssembly e chiamalo da JavaScript.

In questa sezione

In questo tutorial scriveremo alcune definizioni Lean sui rettangoli, dimostreremo un fatto che le riguarda, ne genereremo con lungo un pacchetto TypeScript (eseguito come WebAssembly) e lo useremo. Il progetto Lean è lo stesso dei tutorial per Go, Python, Swift e C.

Prima di iniziare

Servono:

  • Node.js 20 o successivo
  • elan, il gestore delle toolchain di Lean
  • il comando lungo
elan toolchain install leanprover/lean4:v4.34.1
brew install machinefabric/tap/lungo   # apt, dnf, Windows, cargo: vedi il riferimento del comando lungo

Scrivi il progetto Lean

Crea una directory con un progetto Lake in lean/:

mkdir shapes && cd shapes
mkdir lean
echo 'leanprover/lean4:v4.34.1' > lean/lean-toolchain

lean/lakefile.toml dichiara una libreria il cui modulo radice Lake compila per impostazione predefinita:

name = "geometry"
version = "0.1.0"
defaultTargets = ["Geometry"]

[[lean_lib]]
name = "Geometry"

lean/Geometry.lean contiene le definizioni e la dimostrazione:

namespace Geometry

structure Rect where
  width : Nat
  height : Nat
deriving Repr

def area (r : Rect) : Nat := r.width * r.height

def scale (k : Nat) (r : Rect) : Rect :=
  { width := k * r.width, height := k * r.height }

/-- Scaling by `k` multiplies the area by `k * k`. -/
theorem area_scale (k : Nat) (r : Rect) : area (scale k r) = k * k * area r := by
  simp only [area, scale]
  exact Nat.mul_mul_mul_comm k r.width k r.height

/-- The rectangle with the largest area, if any. -/
def largest (rs : List Rect) : Option Rect :=
  rs.foldl (fun best r => match best with
    | some b => if area r > area b then some r else some b
    | none => some r) none

end Geometry

Crea una volta il manifest di Lake (fa parte del progetto):

(cd lean && lake update)

Genera il pacchetto

lungo.toml indica il progetto Lake e dove va il pacchetto npm:

project = "lean"

[ts]
out = "geometry-js"

lungo generate

La prima esecuzione compila il progetto Lean, e quindi controlla la dimostrazione: cambia k * k in k nel teorema e lungo generate fallisce con l’errore di Lean. Scarica anche il wasi-sdk fissato (una volta sola; il suo digest viene controllato) e collega il programma in geometry-js/program.wasm. Aggiungi .lungo/ (lo spazio di lavoro di lungo) a .gitignore.

Chiamalo da JavaScript

Il package.json dell’applicazione:

{ "type": "module", "dependencies": { "geometry": "file:./geometry-js" } }

shapes.js:

import { load } from "geometry";

const geometry = await load();
const r = { width: 3n, height: 4n };
console.log("area:", geometry.area(r));
const bigger = geometry.scale(10n, r);
console.log("scaled:", bigger);
console.log("largest:", geometry.largest([r, bigger]));

$ npm install && node shapes.js
area: 12n
scaled: { width: 30n, height: 40n }
largest: { width: 30n, height: 40n }

Nat è diventato bigint, la structure un oggetto semplice e Option un valore oppure null; index.d.ts fornisce i tipi a TypeScript. Node.js può stampare un ExperimentalWarning su WASI, su cui esegue il modulo. In un browser, load() scarica program.wasm accanto al modulo e lo esegue sul WASI minimale di lungo-ts.

Che cosa abbiamo fatto

Abbiamo generato un pacchetto npm da un progetto Lake di cui Lean ha controllato le dimostrazioni; i suoi metodi eseguono il codice compilato di Lean, compilato in WebAssembly insieme al runtime di lungo. Prossimi passi: