@@ -641,61 +641,15 @@ def checkForManifestMismatch : IO.CacheM Unit := do
641641 precedence, then run `lake update`."
642642 IO.Process.exit 1
643643
644- /-- Fetches the ProofWidgets cloud release and prunes non-JS files. -/
645- def getProofWidgets (buildDir : FilePath) : IO Unit := do
646- if (← buildDir.pathExists) then
647- -- Check if the ProofWidgets build is out-of-date via `lake`.
648- -- This is done through Lake as cache has no simple heuristic
649- -- to determine whether the ProofWidgets JS is out-of-date.
650- let out ← IO.Process.output
651- {cmd := "lake" , args := #["-v" , "build" , "--no-build" , "proofwidgets:release" ]}
652- if out.exitCode == 0 then -- up-to-date
653- return
654- else if out.exitCode == 3 then -- needs fetch (`--no-build` triggered)
655- pure ()
656- else
657- printLakeOutput out
658- throw <| IO.userError s! "Failed to validate ProofWidgets cloud release: \
659- lake failed with error code { out.exitCode} "
660- -- Download and unpack the ProofWidgets cloud release (for its `.js` files)
661- IO.print "Fetching ProofWidgets cloud release..."
662- let out ← IO.Process.output
663- {cmd := "lake" , args := #["-v" , "build" , "proofwidgets:release" ]}
664- if out.exitCode == 0 then
665- IO.println " done!"
666- else
667- IO.print "\n "
668- printLakeOutput out
669- throw <| IO.userError s! "Failed to fetch ProofWidgets cloud release: \
670- lake failed with error code { out.exitCode} "
671- -- Prune non-JS ProofWidgets files (e.g., `olean`, `.c`)
672- try
673- IO.FS.removeDirAll (buildDir / "lib" )
674- IO.FS.removeDirAll (buildDir / "ir" )
675- catch e =>
676- throw <| IO.userError s! "Failed to prune ProofWidgets cloud release: { e} "
677- where
678- printLakeOutput out := do
679- unless out.stdout.isEmpty do
680- IO.eprintln "lake stdout:"
681- IO.eprint out.stdout
682- unless out.stderr.isEmpty do
683- IO.eprintln "lake stderr:"
684- IO.eprint out.stderr
685-
686644/-- Downloads missing files, and unpacks files. -/
687645def getFiles
688646 (repo? : Option String) (hashMap : IO.ModuleHashMap)
689- (forceDownload forceUnpack parallel decompress skipProofWidgets : Bool)
647+ (forceDownload forceUnpack parallel decompress : Bool)
690648 : IO.CacheM Unit := do
691649 let isMathlibRoot ← IO.isMathlibRoot
692650 unless isMathlibRoot do
693651 checkForToolchainMismatch
694652 checkForManifestMismatch
695- if skipProofWidgets then
696- IO.println "Skipping ProofWidgets release fetch"
697- else
698- getProofWidgets (← read).proofWidgetsBuildDir
699653
700654 let mathlibDepPath := (← read).mathlibDepPath
701655
0 commit comments