diff --git a/doc/std/grove/.gitignore b/doc/std/grove/.gitignore index 62842b5f6f..a513c8a64c 100644 --- a/doc/std/grove/.gitignore +++ b/doc/std/grove/.gitignore @@ -1,2 +1,4 @@ /.lake -!lake-manifest.json \ No newline at end of file +!lake-manifest.json +metadata.json +invalidated.json \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Generated.lean b/doc/std/grove/GroveStdlib/Generated.lean index cf991e636f..464366a113 100644 --- a/doc/std/grove/GroveStdlib/Generated.lean +++ b/doc/std/grove/GroveStdlib/Generated.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ import Grove.Framework open Grove.Framework Widget diff --git a/doc/std/grove/GroveStdlib/Generated/Generated b/doc/std/grove/GroveStdlib/Generated/Generated deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/doc/std/grove/GroveStdlib/Root.lean b/doc/std/grove/GroveStdlib/Root.lean deleted file mode 100644 index 92441bca71..0000000000 --- a/doc/std/grove/GroveStdlib/Root.lean +++ /dev/null @@ -1,10 +0,0 @@ -import Grove.Framework - -open Grove.Framework Widget - -namespace GroveStdlib - -def root : Node := - .section "stdlib" "The Lean standard library" #[] - -end GroveStdlib diff --git a/doc/std/grove/GroveStdlib/Std.lean b/doc/std/grove/GroveStdlib/Std.lean new file mode 100644 index 0000000000..e8c290889a --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import GroveStdlib.Std.CoreTypesAndOperations +import GroveStdlib.Std.LanguageConstructs +import GroveStdlib.Std.Libraries +import GroveStdlib.Std.OperatingSystemAbstractions + +open Grove.Framework Widget + +namespace GroveStdlib + +namespace Std + +def introduction : Node := + .text "Welcome to the interactive Lean standard library outline!" + +end Std + +def std : Node := + .section "stdlib" "The Lean standard library" #[ + Std.introduction, + Std.coreTypesAndOperations, + Std.languageConstructs, + Std.libraries, + Std.operatingSystemAbstractions + ] + +end GroveStdlib diff --git a/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations.lean b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations.lean new file mode 100644 index 0000000000..047c76b8f5 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework +import GroveStdlib.Std.CoreTypesAndOperations.BasicTypes +import GroveStdlib.Std.CoreTypesAndOperations.Containers +import GroveStdlib.Std.CoreTypesAndOperations.Numbers +import GroveStdlib.Std.CoreTypesAndOperations.StringsAndFormatting + +open Grove.Framework Widget + +namespace GroveStdlib.Std + +namespace CoreTypesAndOperations + +end CoreTypesAndOperations + +def coreTypesAndOperations : Node := + .section "core-types-and-operations" "Core types and operations" #[ + CoreTypesAndOperations.basicTypes, + CoreTypesAndOperations.containers, + CoreTypesAndOperations.numbers, + CoreTypesAndOperations.stringsAndFormatting + ] + +end GroveStdlib.Std diff --git a/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/BasicTypes.lean b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/BasicTypes.lean new file mode 100644 index 0000000000..ec5a7ad3dd --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/BasicTypes.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.CoreTypesAndOperations + +namespace BasicTypes + +end BasicTypes + +def basicTypes : Node := + .section "basic-types" "Basic types" #[] + +end GroveStdlib.Std.CoreTypesAndOperations diff --git a/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean new file mode 100644 index 0000000000..9857617455 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.CoreTypesAndOperations + +namespace Containers + +end Containers + +def containers : Node := + .section "containers" "Containers" #[] + +end GroveStdlib.Std.CoreTypesAndOperations \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Numbers.lean b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Numbers.lean new file mode 100644 index 0000000000..18e874d520 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Numbers.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.CoreTypesAndOperations + +namespace Numbers + +end Numbers + +def numbers : Node := + .section "numbers" "Numbers" #[] + +end GroveStdlib.Std.CoreTypesAndOperations \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/StringsAndFormatting.lean b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/StringsAndFormatting.lean new file mode 100644 index 0000000000..3e40a80766 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/StringsAndFormatting.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.CoreTypesAndOperations + +namespace StringsAndFormatting + +end StringsAndFormatting + +def stringsAndFormatting : Node := + .section "strings-and-formatting" "Strings and formatting" #[] + +end GroveStdlib.Std.CoreTypesAndOperations \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/LanguageConstructs.lean b/doc/std/grove/GroveStdlib/Std/LanguageConstructs.lean new file mode 100644 index 0000000000..9810f6b4de --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/LanguageConstructs.lean @@ -0,0 +1,26 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework +import GroveStdlib.Std.LanguageConstructs.ComparisonOrderingHashing +import GroveStdlib.Std.LanguageConstructs.Monads +import GroveStdlib.Std.LanguageConstructs.RangesAndIterators + +open Grove.Framework Widget + +namespace GroveStdlib.Std + +namespace LanguageConstructs + +end LanguageConstructs + +def languageConstructs : Node := + .section "language-constructs" "Language constructs" #[ + LanguageConstructs.comparisonOrderingHashing, + LanguageConstructs.monads, + LanguageConstructs.rangesAndIterators + ] + +end GroveStdlib.Std diff --git a/doc/std/grove/GroveStdlib/Std/LanguageConstructs/ComparisonOrderingHashing.lean b/doc/std/grove/GroveStdlib/Std/LanguageConstructs/ComparisonOrderingHashing.lean new file mode 100644 index 0000000000..9cc919d349 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/LanguageConstructs/ComparisonOrderingHashing.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.LanguageConstructs + +namespace ComparisonOrderingHashing + +end ComparisonOrderingHashing + +def comparisonOrderingHashing : Node := + .section "comparison-ordering-hashing" "Comparison, ordering, hashing" #[] + +end GroveStdlib.Std.LanguageConstructs \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/LanguageConstructs/Monads.lean b/doc/std/grove/GroveStdlib/Std/LanguageConstructs/Monads.lean new file mode 100644 index 0000000000..9e32239350 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/LanguageConstructs/Monads.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.LanguageConstructs + +namespace Monads + +end Monads + +def monads : Node := + .section "monads" "Monads" #[] + +end GroveStdlib.Std.LanguageConstructs \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/LanguageConstructs/RangesAndIterators.lean b/doc/std/grove/GroveStdlib/Std/LanguageConstructs/RangesAndIterators.lean new file mode 100644 index 0000000000..53058613e9 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/LanguageConstructs/RangesAndIterators.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.LanguageConstructs + +namespace RangesAndIterators + +end RangesAndIterators + +def rangesAndIterators : Node := + .section "ranges-and-iterators" "Ranges and iterators" #[] + +end GroveStdlib.Std.LanguageConstructs \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/Libraries.lean b/doc/std/grove/GroveStdlib/Std/Libraries.lean new file mode 100644 index 0000000000..67ced13259 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/Libraries.lean @@ -0,0 +1,24 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework +import GroveStdlib.Std.Libraries.DateAndTime +import GroveStdlib.Std.Libraries.RandomNumbers + +open Grove.Framework Widget + +namespace GroveStdlib.Std + +namespace Libraries + +end Libraries + +def libraries : Node := + .section "libraries" "Libraries" #[ + Libraries.dateAndTime, + Libraries.randomNumbers + ] + +end GroveStdlib.Std diff --git a/doc/std/grove/GroveStdlib/Std/Libraries/DateAndTime.lean b/doc/std/grove/GroveStdlib/Std/Libraries/DateAndTime.lean new file mode 100644 index 0000000000..467da02e9a --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/Libraries/DateAndTime.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.Libraries + +namespace DateAndTime + +end DateAndTime + +def dateAndTime : Node := + .section "date-and-time" "Date and time" #[] + +end GroveStdlib.Std.Libraries \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/Libraries/RandomNumbers.lean b/doc/std/grove/GroveStdlib/Std/Libraries/RandomNumbers.lean new file mode 100644 index 0000000000..783f75eef6 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/Libraries/RandomNumbers.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.Libraries + +namespace RandomNumbers + +end RandomNumbers + +def randomNumbers : Node := + .section "random-numbers" "Random numbers" #[] + +end GroveStdlib.Std.Libraries \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions.lean b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions.lean new file mode 100644 index 0000000000..3bcdafdba5 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions.lean @@ -0,0 +1,30 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework +import GroveStdlib.Std.OperatingSystemAbstractions.AsynchronousIO +import GroveStdlib.Std.OperatingSystemAbstractions.BasicIO +import GroveStdlib.Std.OperatingSystemAbstractions.ConcurrencyAndParallelism +import GroveStdlib.Std.OperatingSystemAbstractions.EnvironmentFileSystemProcesses +import GroveStdlib.Std.OperatingSystemAbstractions.Locales + +open Grove.Framework Widget + +namespace GroveStdlib.Std + +namespace OperatingSystemAbstractions + +end OperatingSystemAbstractions + +def operatingSystemAbstractions : Node := + .section "operating-system-abstractions" "Operating system abstractions" #[ + OperatingSystemAbstractions.asynchronousIO, + OperatingSystemAbstractions.basicIO, + OperatingSystemAbstractions.concurrencyAndParallelism, + OperatingSystemAbstractions.environmentFileSystemProcesses, + OperatingSystemAbstractions.locales + ] + +end GroveStdlib.Std diff --git a/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/AsynchronousIO.lean b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/AsynchronousIO.lean new file mode 100644 index 0000000000..61d8eaea4b --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/AsynchronousIO.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.OperatingSystemAbstractions + +namespace AsynchronousIO + +end AsynchronousIO + +def asynchronousIO : Node := + .section "asynchronous-io" "Asynchronous I/O" #[] + +end GroveStdlib.Std.OperatingSystemAbstractions \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/BasicIO.lean b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/BasicIO.lean new file mode 100644 index 0000000000..a895c778b4 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/BasicIO.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.OperatingSystemAbstractions + +namespace BasicIO + +end BasicIO + +def basicIO : Node := + .section "basic-io" "Basic I/O" #[] + +end GroveStdlib.Std.OperatingSystemAbstractions \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/ConcurrencyAndParallelism.lean b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/ConcurrencyAndParallelism.lean new file mode 100644 index 0000000000..150aba8b93 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/ConcurrencyAndParallelism.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.OperatingSystemAbstractions + +namespace ConcurrencyAndParallelism + +end ConcurrencyAndParallelism + +def concurrencyAndParallelism : Node := + .section "concurrency-and-parallelism" "Concurrency and parallelism" #[] + +end GroveStdlib.Std.OperatingSystemAbstractions \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/EnvironmentFileSystemProcesses.lean b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/EnvironmentFileSystemProcesses.lean new file mode 100644 index 0000000000..0c6a7ee7ab --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/EnvironmentFileSystemProcesses.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.OperatingSystemAbstractions + +namespace EnvironmentFileSystemProcesses + +end EnvironmentFileSystemProcesses + +def environmentFileSystemProcesses : Node := + .section "environment-filesystem-processes" "Environment, file system, processes" #[] + +end GroveStdlib.Std.OperatingSystemAbstractions \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/Locales.lean b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/Locales.lean new file mode 100644 index 0000000000..a4ab2251c8 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/Locales.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import Grove.Framework + +open Grove.Framework Widget + +namespace GroveStdlib.Std.OperatingSystemAbstractions + +namespace Locales + +end Locales + +def locales : Node := + .section "locales" "Locales" #[] + +end GroveStdlib.Std.OperatingSystemAbstractions \ No newline at end of file diff --git a/doc/std/grove/Main.lean b/doc/std/grove/Main.lean index a148fbc69d..7cf42d7ccb 100644 --- a/doc/std/grove/Main.lean +++ b/doc/std/grove/Main.lean @@ -1,4 +1,9 @@ -import GroveStdlib.Root +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import GroveStdlib.Std import GroveStdlib.Generated def config : Grove.Framework.Project.Configuration where @@ -6,7 +11,7 @@ def config : Grove.Framework.Project.Configuration where def project : Grove.Framework.Project where config := config - rootNode := GroveStdlib.root + rootNode := GroveStdlib.std restoreState := GroveStdlib.Generated.restoreState def main (args : List String) : IO UInt32 := diff --git a/doc/std/grove/grove-local.sh b/doc/std/grove/grove-local.sh new file mode 100755 index 0000000000..175af37249 --- /dev/null +++ b/doc/std/grove/grove-local.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +lake exe grove-stdlib --full metadata.json +cd .lake/packages/grove/frontend +npm install +if [ -f "../../../../invalidated.json" ]; then + GROVE_DATA_LOCATION=../../../../metadata.json GROVE_UPSTREAM_INVALIDATED_FACTS_LOCATION=../../../../invalidated.json npm run dev +else + GROVE_DATA_LOCATION=../../../../metadata.json npm run dev +fi \ No newline at end of file diff --git a/doc/std/grove/lake-manifest.json b/doc/std/grove/lake-manifest.json index 0182c0568c..1d3cbacf30 100644 --- a/doc/std/grove/lake-manifest.json +++ b/doc/std/grove/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": "backend", "scope": "", - "rev": "3a2347d170599f500cb34a82676e078d8b4a076e", + "rev": "78110476d9c76abd4103d91a0ae3f89405558065", "name": "grove", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/doc/std/grove/update_invalidated.sh b/doc/std/grove/update_invalidated.sh new file mode 100755 index 0000000000..17a2030f0e --- /dev/null +++ b/doc/std/grove/update_invalidated.sh @@ -0,0 +1,3 @@ +#!/bin/sh + +lake exe grove-stdlib --invalidated invalidated.json \ No newline at end of file