Documentazione di lungo

La tua prima libreria C costruita da Lean

Scrivi definizioni Lean e una dimostrazione, genera da esse una libreria C con lungo e chiamala da un programma C compilato con CMake.

In questa sezione

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

Prima di iniziare

Servono:

  • CMake 3.20 o successivo e un compilatore C11
  • 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 la libreria

lungo.toml indica il progetto Lake e dove va la libreria C:

project = "lean"

[c]
out = "geometry-c"

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-c è un progetto CMake della libreria geometry, la cui API è include/geometry.h; aggiungi .lungo/ (lo spazio di lavoro di lungo) a .gitignore.

Chiamala da C

Il CMakeLists.txt del programma:

cmake_minimum_required(VERSION 3.20)
project(shapes C)
add_subdirectory(geometry-c)
add_executable(shapes main.c)
target_link_libraries(shapes PRIVATE geometry)

main.c:

#include <stdio.h>
#include <stdlib.h>

#include "geometry.h"

/* Exits with the error of a failed call. */
static lungo_value *check(int32_t status, lungo_value *result, lungo_error *error) {
    if (status != LUNGO_OK) {
        fprintf(stderr, "error: %s\n", lungo_error_message(error));
        exit(1);
    }
    return result;
}

static void print_rect(const char *label, const lungo_value *r) {
    char *w = lungo_value_number_string(geometry_rect_width(r));
    char *h = lungo_value_number_string(geometry_rect_height(r));
    printf("%s: %s x %s\n", label, w, h);
    lungo_string_free(w);
    lungo_string_free(h);
}

int main(void) {
    lungo_value *result = NULL;
    lungo_error *error = NULL;

    lungo_value *r = geometry_rect_mk(lungo_value_nat(3), lungo_value_nat(4));
    lungo_value *area = check(geometry_area(r, &result, &error), result, error);
    char *digits = lungo_value_number_string(area);
    printf("area: %s\n", digits);
    lungo_string_free(digits);

    lungo_value *ten = lungo_value_nat(10);
    lungo_value *bigger = check(geometry_scale(ten, r, &result, &error), result, error);
    print_rect("scaled", bigger);

    lungo_value *items[2] = {lungo_value_clone(r), lungo_value_clone(bigger)};
    lungo_value *list = lungo_value_list(items, 2);
    lungo_value *best = check(geometry_largest(list, &result, &error), result, error);
    if (lungo_value_get_option(best)) print_rect("largest", lungo_value_get_option(best));

    lungo_value_free(best);
    lungo_value_free(list);
    lungo_value_free(bigger);
    lungo_value_free(ten);
    lungo_value_free(area);
    lungo_value_free(r);
    return 0;
}

$ cmake -S . -B build && cmake --build build && ./build/shapes
area: 12
scaled: 30 x 40
largest: 30 x 40

CMake scarica il runtime di lungo per la piattaforma e ne controlla il digest SHA-256 prima di collegarlo. Ogni valore Lean è un lungo_value: i costruttori (geometry_rect_mk) prendono possesso delle loro parti, gli accessori (geometry_rect_width) le prendono in prestito, e ogni valore restituito dall’API va liberato una volta.

Che cosa abbiamo fatto

Abbiamo generato una libreria C da un progetto Lake di cui Lean ha controllato le dimostrazioni; esegue il codice compilato di Lean sul runtime di lungo. Prossimi passi: