Hacktoberfest 2026 : les issues que les mainteneurs ont marquées pour octobre, ouvertes et accessibles aux débutants. Parcourir les issues Hacktoberfest

Migrate tests from hand-rolled IO to LSpec framework

Ouverte
  • Quelque chose ne va pas ?
#7 0 commentaires 0 réactions 0 personnes assignées Voir sur GitHub

Personne n'a encore pris cette issue.

Évaluation

Difficulté
4/5
Temps estimé
3-5 jours
Accessibilité débutants
42/100
Type d'issue
Refactorisation
Clarté
Plutôt claire
Activité
À l'abandon
Domaine
build-system, testing

Piste de recherche

Commencez par lire test/ParserTest.lean, test/NfaTest.lean, test/MatcherTest.lean et test/Main.lean afin de comprendre les 67 tests existants et leurs points d’entrée actuels. Examinez ensuite lakefile.toml et les exigences d’intégration de LSpec. La tâche est terminée lorsque les tests utilisent des suites LSpec groupées, que lake test fournit des résultats structurés et que le scaffolding IO manuel est supprimé.

Rédigé par le modèle d'indexation à partir du texte de l'issue.

Description

Summary

The current test suite uses hand-rolled IO Unit functions with manual IO.println "✓" / throw "✗" for pass/fail reporting. This reimplements scaffolding that existing Lean 4 testing frameworks already provide.

Current state

  • 67 tests across ParserTest.lean, NfaTest.lean, MatcherTest.lean
  • Each test is a def testFoo : IO Unit that manually prints results
  • test/Main.lean calls each test function sequentially
  • No structured output, no test counts, no failure summaries

Recommended approach: LSpec

LSpec is the standard Lean 4 testing framework. Tests become declarative assertions:

import LSpec
import Lck.Regex.Parser

def parserSuite := [
    test "single char" (parse "a" = Except.ok (Regex.char 'a')),
    test "reversed range fails" (parse "[z-a]" matches Except.error _),
    test "empty pattern" (parse "" = Except.error RegexError.emptyPattern)
  ]

def main := lspecIO $ .ofList [
    ("parser", parserSuite),
    ("matcher", matcherSuite)
  ]

Benefits:

  • Eliminates ~200 lines of boilerplate (manual IO.println/throw per test)
  • Structured pass/fail output with counts and summaries
  • Standard lake test integration via testDriver
  • Consistent with Lean ecosystem conventions

Other approaches worth considering

  • #guard: Built-in compile-time assertions (#guard parse "a" = Except.ok (Regex.char 'a')). Zero boilerplate, failures are compilation errors. Good for simple invariants alongside LSpec.
  • SlimCheck/Plausible: Property-based testing for discovering edge cases automatically. Could complement LSpec for properties like "any regex that parses successfully can be compiled to an NFA".

Migration plan

  1. Add LSpec dependency to lakefile.toml
  2. Convert each testFoo : IO Unit to an LSpec test "name" (assertion)
  3. Group tests into suites by module
  4. Wire up main := lspecIO $ .ofList [...]
  5. Configure testDriver in lakefile
  6. Remove manual IO scaffolding
Langage dominant
Lean
Étoiles
2
Forks
1
Aucune PR mergée en 30 j

Préparer son environnement

Ce projet ne fournit ni conteneur de développement, ni Dockerfile, ni guide de contribution : l'installation est à votre charge. Commencez par son README, et consultez notre guide de la première contribution pour les étapes générales.

Par où commencer

  1. Lisez l'issue en entier, puis le guide de contribution du projet.
  2. Signalez en commentaire que vous la prenez — cela évite que deux personnes fassent le même travail.
  3. Forkez le dépôt et travaillez sur une branche.
  4. Ouvrez une pull request qui référence le numéro de l'issue.

Autres issues de lambdaclass/lambda_compiler_kit

Toutes les issues de lambdaclass/lambda_compiler_kit

Issues similaires

Plus d'issues Build System

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.