Documentazione di lungo

Il tuo primo pacchetto Swift costruito da Lean

Scrivi definizioni Lean e una dimostrazione, genera da esse un pacchetto Swift con lungo e chiamalo da Swift.

In questa sezione

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

Prima di iniziare

Servono:

  • Xcode o una toolchain Swift 5.9 su un Mac
  • 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 Swift:

project = "lean"

[swift]
out = "geometry-swift"

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. geometry-swift è un pacchetto Swift con il prodotto Geometry; aggiungi .lungo/ (lo spazio di lavoro di lungo) a .gitignore.

Chiamalo da Swift

Un pacchetto da riga di comando accanto a esso, Package.swift:

// swift-tools-version:5.9
import PackageDescription

let package = Package(
    name: "Shapes",
    platforms: [.macOS("12.0")],
    dependencies: [.package(path: "geometry-swift")],
    targets: [
        .executableTarget(name: "Shapes", dependencies: [.product(name: "Geometry", package: "geometry-swift")])
    ]
)

Sources/Shapes/main.swift:

import Geometry

let r = Rect(width: 3, height: 4)
print("area:", try area(r))
let bigger = try scale(10, r)
print("scaled:", bigger.width, "x", bigger.height)
if let best = try largest([r, bigger]) {
    print("largest:", best.width, "x", best.height)
}

$ swift run
area: 12
scaled: 30 x 40
largest: 30 x 40

La structure è diventata una struct Swift, Nat un LungoNat (con letterali interi), Option un opzionale, e ogni funzione è throws. Il codice Objective-C usa lo stesso pacchetto tramite la sua API C: @import GeometryProgram;.

Che cosa abbiamo fatto

Abbiamo generato un pacchetto Swift da un progetto Lake di cui Lean ha controllato le dimostrazioni; esegue il codice compilato di Lean sul runtime di lungo, che lungo-swift fornisce come XCFramework. Prossimi passi: