الاختبار في مسار Lean

تشغيل الاختبارات

لتشغيل الاختبارات، تأكد من أن 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]

في هذا المثال، يستورد ملف الاختبار في السطر 2 وحدةً تُدعى ExerciseName. ويستدعي الاختبار first test دالةً هي ExerciseName.someFun بوسيطين هما someArg1 وsomeArg2. وExerciseName التي تسبق someFun هي فضاء أسماء، مُعرَّف في الوحدة التي تحمل الاسم نفسه، أي ExerciseName. وهذا يعني أنه عليك إنشاء ملف باسم ExerciseName.lean يبدو هكذا:

namespace ExerciseName

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

end ExerciseName

لاحظ أن الاختبارات عادةً تستدعي دالة أو أكثر بعدد من الوسائط. ويُتوقَّع أن تكون جميعها مُعرَّفة في وحدة الحل، داخل فضاء أسماء يحمل الاسم نفسه الذي تحمله الوحدة.

لكل وسيط ولكل قيمة مُرجعة من كل دالة نوعٌ ما. قد يكون أحد الأنواع الأساسية في Lean (مثل Nat أو List Int أو Option String)، أو نوعًا يعرّفه المستخدم.

ستجد ملفًا بالاسم الصحيح موجودًا بالفعل في المجلد نفسه الذي توجد فيه وحدة الاختبار. ومن المفترض أن يحتوي هذا الملف على هيكل يتضمّن معظم المعلومات الأولية، حتى تستخدمه كنقطة انطلاق لحلك.

تذكّر فقط أن هذا الهيكل موجود لمساعدتك على البدء فحسب. ولا تتردد في تغييره بالكامل إذا رأيت أن ذلك هو الصواب.

استخدام الحزم

يمكن لمشاريع Lean التي تستخدم Lake أن تستورد دائمًا المكتبة القياسية Std، التي تحتوي على هياكل بيانات إضافية، وواجهات الإدخال/الإخراج وواجهات APIs للنظام، وأدوات مساعدة أساسية أخرى. ويجب أن يكون هذا الاستيراد في بداية الملف:

import Std

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

في هذا المثال، النوع HashMap مُقيَّد بـ Std، وهو فضاء الأسماء الذي عُرِّف فيه. وجميع الموارد في المكتبة القياسية تقع في فضاء الأسماء نفسه، Std.

ويمكنك أيضًا فتح وحدة بحيث تصبح جميع هياكل بياناتها ودوالها متاحة دون هذا التقييد بفضاء الأسماء:

import Std

open Std

def someSet : TreeSet String := ...

الحزم الخارجية ليست متاحة مباشرة، ويجب إضافتها كتبعية في lakefile.toml.

أثناء عملك محليًا، يمكنك استخدام أي حزمة تشاء. أما مشغّل الاختبارات عبر الإنترنت، فلا يتاح له سوى المكتبة القياسية Std.