Documentation for Lean Version Upgrade

Aperta
  • Qualcosa non va?
#280 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
4/5
Tempo stimato
3-5 giorni
Idoneità per principianti
30/100
Tipo di issue
Documentazione
Chiarezza
Abbastanza chiara
Stato di attività
Ferma
Ambito
build-system, compilers, documentation

Direzione di ricerca

Inizia riproducendo i risultati segnalati di lake run setup e lake update dopo aver recuperato main, quindi esamina lake-packages/YatimaStdLib/lakefile.lean e la documentazione di setup esistente del progetto. Il lavoro è completato quando la procedura di aggiornamento alla versione supportata di Lean è documentata con sufficiente chiarezza da permettere agli utenti di evitare o comprendere gli errori del manifest e dell'API Lake.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

Since Yatima is not currently in active development, it would be great to have documentation on how to upgrade the Lean version of the current project so that user may be able to still use compiler as the lake upgrade command suggested after lake run setup does not seem to bump everything properly.

Currently after pulling main and running lake run setup produces

warning: improperly formatted manifest: incompatible manifest version `4`
error: dependency 'LSpec' of 'Yatima' not in manifest, use `lake update` to update

while running lake update produces

warning: improperly formatted manifest: incompatible manifest version `4`
error: ./lake-packages/YatimaStdLib/lakefile.lean:14:15: error: invalid field 'oleanDir', the environment does not contain 'Lake.Package.oleanDir'
  pkg
has type
  Package
error: ./lake-packages/YatimaStdLib/lakefile.lean:23:33: error: unknown identifier 'defaultLibDir'
error: ./lake-packages/YatimaStdLib/lakefile.lean:23:57: error: application type mismatch
  List.cons job
argument
  job
has type
  CustomData (Package.name pkg, `importTarget) : Type
but is expected to have type
  BuildJob FilePath : Type
error: ./lake-packages/YatimaStdLib/lakefile.lean: package configuration has errors

Might be an issue with Lean4 Arch (AUR) package, however.

Lingua principale
Lean
Stelle
148
Fork
12
Nessuna PR unita negli ultimi 30g

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di argumentcomputer/yatima

Tutte le issue di argumentcomputer/yatima

Issue simili

Altre issue su Build System

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.