टेस्ट चलाना
टेस्ट चलाने के लिए यह ज़रूरी है कि आपके सिस्टम पर Lean 4 इंस्टॉल हो।
अभ्यास वाली डायरेक्टरी में जाकर यह चलाइए:
lake test
अभ्यास हल करना
किसी अभ्यास का हल एक Lean मॉड्यूल होता है।
मॉड्यूल का नाम टेस्ट सूट की शुरुआत में एक इंपोर्ट स्टेटमेंट में दिया होता है:
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]
इस उदाहरण में टेस्ट फाइल दूसरी लाइन में ExerciseName नाम का एक मॉड्यूल इंपोर्ट करती है।
first test टेस्ट ExerciseName.someFun फंक्शन को someArg1 और someArg2 आर्गुमेंट के साथ कॉल करता है।
someFun से पहले लिखा यह ExerciseName एक नेमस्पेस है, जो उसी नाम वाले मॉड्यूल में परिभाषित होता है, यानी ExerciseName मॉड्यूल में।
इसका मतलब है कि आपको ExerciseName.lean नाम की एक फाइल बनानी होगी, जो कुछ इस तरह दिखेगी:
namespace ExerciseName
def someFun (someArg1 : Type1) (someArg2 : Type2) : ReturnType :=
...
end ExerciseName
ध्यान दीजिए कि टेस्ट आम तौर पर एक या अधिक फंक्शन को कई आर्गुमेंट के साथ कॉल करते हैं।
इन सभी को हल वाले मॉड्यूल में, मॉड्यूल के ही नाम वाले नेमस्पेस के अंदर परिभाषित होना चाहिए।
हर आर्गुमेंट का और हर फंक्शन की रिटर्न वैल्यू का एक टाइप होता है।
यह Lean के बुनियादी टाइपों में से कोई एक हो सकता है (जैसे Nat, List Int या Option String), या उपयोगकर्ता द्वारा बनाया गया कोई टाइप हो सकता है।
टेस्ट मॉड्यूल वाले ही फोल्डर में आपको सही नाम वाली एक फाइल पहले से मौजूद मिलेगी।
इस फाइल में ज़्यादातर शुरुआती जानकारी वाला एक स्टब होना चाहिए, ताकि आप उसे अपने हल की शुरुआत के तौर पर इस्तेमाल कर सकें।
बस ध्यान रखिए कि यह स्टब सिर्फ इसलिए है कि आप शुरुआत कर सकें।
अगर आपको लगता है कि इसे पूरी तरह बदलना सही है, तो आप इसे पूरी तरह बदल सकते हैं।
पैकेज इस्तेमाल करना
Lake इस्तेमाल करने वाले Lean प्रोजेक्ट हमेशा Std स्टैंडर्ड लाइब्रेरी इंपोर्ट कर सकते हैं, जिसमें अतिरिक्त डेटा स्ट्रक्चर, I/O और सिस्टम API, तथा अन्य बुनियादी सुविधाएँ शामिल हैं।
यह इंपोर्ट फाइल की शुरुआत में होना चाहिए:
import Std
def someMap : Std.HashMap Int Nat := ...
इस उदाहरण में HashMap टाइप के साथ Std लगा है, यानी वह नेमस्पेस जहाँ यह परिभाषित होता है।
स्टैंडर्ड लाइब्रेरी की सभी चीज़ें एक ही नेमस्पेस, Std, में होती हैं।
किसी मॉड्यूल को खोलना भी संभव है, ताकि उसके सभी डेटा स्ट्रक्चर और फंक्शन इस नेमस्पेस क्वालिफिकेशन के बिना उपलब्ध रहें:
import Std
open Std
def someSet : TreeSet String := ...
बाहरी पैकेज सीधे उपलब्ध नहीं होते, उन्हें lakefile.toml में डिपेंडेंसी के तौर पर जोड़ना पड़ता है।
स्थानीय तौर पर काम करते समय आप अपनी पसंद का कोई भी पैकेज इस्तेमाल कर सकते हैं।
लेकिन ऑनलाइन टेस्ट रनर के पास सिर्फ Std स्टैंडर्ड लाइब्रेरी तक ही पहुँच है।
