Lean ট্র্যাকে টেস্ট করা

টেস্ট চালানো

টেস্ট চালাতে হলে, আপনার Lean 4 ইনস্টল করা আছে কি না নিশ্চিত হয়ে নিন।

অনুশীলনীর ডিরেক্টরি থেকে রান করুন:

lake test

অনুশীলনীটি সমাধান করা

একটি অনুশীলনীর সমাধান হলো একটি Lean মডিউল। মডিউলের নাম নির্ধারণ করা হয় টেস্ট স্যুটের শুরুতে একটি import statement-এ:

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 টেস্টটি someArg1 ও someArg2 আর্গুমেন্ট দিয়ে ExerciseName.someFun ফাংশনটি কল করে। someFun-এর আগের এই ExerciseName হলো একটি নেমস্পেস, যা একই নামের মডিউলে, অর্থাৎ ExerciseName-এ ডিফাইন করা হয়েছে। এর মানে হলো, আপনার ExerciseName.lean নামের একটি ফাইল তৈরি করতে হবে, যা দেখতে এমন হবে:

namespace ExerciseName

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

end ExerciseName

লক্ষ্য করুন, টেস্ট সাধারণত এক বা একাধিক ফাংশনকে কিছু সংখ্যক আর্গুমেন্ট দিয়ে কল করে। এদের সবগুলোই সমাধান মডিউলে, মডিউলের সমান নামের একটি নেমস্পেসের ভেতরে ডিফাইন করা থাকবে বলে আশা করা হয়।

প্রতিটি আর্গুমেন্ট এবং প্রতিটি ফাংশনের রিটার্ন ভ্যালুর একটি নির্দিষ্ট টাইপ থাকে। এটি Lean-এর মৌলিক টাইপগুলোর একটি হতে পারে (যেমন Nat, List Int বা Option String), অথবা ব্যবহারকারীর সংজ্ঞায়িত একটি টাইপ।

টেস্ট মডিউলের মতো একই ফোল্ডারে সঠিক নামের একটি ফাইল আগে থেকেই পেয়ে যাবেন। এই ফাইলে বেশিরভাগ প্রাথমিক তথ্যসহ একটি stub থাকবে, যাতে আপনি এটিকে আপনার সমাধানের সূচনা বিন্দু হিসেবে ব্যবহার করতে পারেন।

শুধু মনে রাখবেন, এই স্টাবটি কেবল আপনার শুরু করার জন্য রাখা হয়েছে। আপনি যদি মনে করেন এটি করাই ঠিক, তবে নির্দ্বিধায় এটিকে পুরোপুরি বদলে ফেলতে পারেন।

প্যাকেজ ব্যবহার করা

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 স্ট্যান্ডার্ড লাইব্রেরির অ্যাক্সেস আছে।