Δοκιμές στη διαδρομή Lean

Εκτέλεση των τεστ

Για να τρέξεις τα τεστ, βεβαιώσου πρώτα ότι έχεις εγκαταστήσει το Lean 4.

Από τον φάκελο της άσκησης, τρέξε:

lake test

Επίλυση της άσκησης

Η λύση μιας άσκησης είναι ένα module της Lean. Το όνομα του module ορίζεται σε μια εντολή import στην αρχή της σουίτας τεστ:

import LeanTest
import ExerciseName

open LeanTest

def exerciseNameTests : TestSuite :=
  (TestSuite.empty "ExerciseName")
  |>.addTest "first test" (do
        return assertEqual someVal (ExerciseName.someFun someArg1 someArg2))
    ...

def main : IO UInt32 := do
  runTestSuitesWithExitCode [exerciseNameTests]

Σε αυτό το παράδειγμα, το αρχείο τεστ εισάγει, στη γραμμή 2, ένα module με το όνομα ExerciseName. Το τεστ first test καλεί μια συνάρτηση ExerciseName.someFun με ορίσματα someArg1 και someArg2. Αυτό το ExerciseName πριν από το someFun είναι ένα namespace, που ορίζεται στο module με το ίδιο όνομα, δηλαδή ExerciseName. Αυτό σημαίνει ότι πρέπει να δημιουργήσεις ένα αρχείο με το όνομα ExerciseName.lean που να μοιάζει κάπως έτσι:

namespace ExerciseName

def someFun (someArg1 : Type1) (someArg2 : Type2) : ReturnType :=
    ...

end ExerciseName

Σημείωσε ότι τα τεστ συνήθως καλούν μία ή περισσότερες συναρτήσεις με κάποιον αριθμό ορισμάτων. Όλες τους αναμένεται να ορίζονται στο module της λύσης, μέσα σε ένα namespace με το ίδιο όνομα με το module.

Κάθε όρισμα και η τιμή επιστροφής κάθε συνάρτησης έχει κάποιον τύπο. Αυτός μπορεί να είναι ένας από τους βασικούς τύπους της Lean (για παράδειγμα, Nat, List Int ή Option String) ή ένας τύπος που ορίζεις ο ίδιος.

Θα βρεις ένα αρχείο με το σωστό όνομα ήδη στη θέση του, στον ίδιο φάκελο με το module των τεστ. Αυτό το αρχείο θα πρέπει να έχει ένα stub με τις περισσότερες αρχικές πληροφορίες, ώστε να το χρησιμοποιήσεις ως σημείο εκκίνησης για τη λύση σου.

Απλώς έχε κατά νου ότι αυτό το stub υπάρχει μόνο για να ξεκινήσεις. Μη διστάσεις να το αλλάξεις εντελώς, αν πιστεύεις ότι αυτό είναι το σωστό.

Χρήση πακέτων

Τα έργα της Lean που χρησιμοποιούν το Lake μπορούν πάντα να εισάγουν την πρότυπη βιβλιοθήκη Std, η οποία περιέχει επιπλέον δομές δεδομένων, I/O και API συστήματος, καθώς και άλλα βασικά βοηθητικά εργαλεία. Αυτή η εισαγωγή πρέπει να βρίσκεται στην αρχή του αρχείου:

import Std

def someMap : Std.HashMap Int Nat := ...

Σε αυτό το παράδειγμα, ο τύπος HashMap χαρακτηρίζεται με πρόθεμα το Std, το namespace όπου ορίζεται. Όλοι οι πόροι της πρότυπης βιβλιοθήκης βρίσκονται στο ίδιο namespace, το Std.

Είναι επίσης δυνατό να ανοίξεις ένα module, ώστε όλες οι δομές δεδομένων και οι συναρτήσεις του να είναι διαθέσιμες χωρίς αυτό το πρόθεμα του namespace:

import Std

open Std

def someSet : TreeSet String := ...

Τα εξωτερικά πακέτα δεν είναι άμεσα διαθέσιμα και πρέπει να προστεθούν ως εξάρτηση στο lakefile.toml.

Όσο δουλεύεις τοπικά, μπορείς να χρησιμοποιήσεις όποιο πακέτο θέλεις. Ο διαδικτυακός εκτελεστής τεστ, ωστόσο, έχει πρόσβαση μόνο στην πρότυπη βιβλιοθήκη Std.