Allow injecting the literate output with datetime info

cli-console/src/main/java/org/aya/cli/console/Main.java

@@ -106,33 +106,31 @@ private int doCompile(@NotNull CompileAction compile) throws IOException {
     return compiler.compile(filePath, null);
   }
 
-  private @Nullable CompilerFlags.PrettyInfo
-  computePrettyInfo(
+  private @Nullable CompilerFlags.PrettyInfo computePrettyInfo(
     @Nullable Path outputPath,
     RenderOptions renderOptions, AyaPrettierOptions prettierOptions
   ) {
-    return prettyStage == null
-      ? (outputPath != null ? CompilerFlags.prettyInfoFromOutput(
-      outputPath, renderOptions, prettyNoCodeStyle, prettyInlineCodeStyle, prettySSR) : null)
-      : new CompilerFlags.PrettyInfo(
-        asciiOnly,
-        prettyNoCodeStyle,
-        prettyInlineCodeStyle,
-        prettySSR,
-        prettyStage,
-        prettyFormat,
-        prettierOptions,
-        renderOptions,
-        prettyDir
-      );
+    if (prettyStage == null)
+      return outputPath != null ? CompilerFlags.prettyInfoFromOutput(
+        outputPath, renderOptions, prettyNoCodeStyle, prettyInlineCodeStyle, prettySSR) : null;
+    return new CompilerFlags.PrettyInfo(
+      asciiOnly,
+      prettyNoCodeStyle,
+      prettyInlineCodeStyle,
+      prettySSR,
+      prettyStage,
+      prettyFormat,
+      prettierOptions, renderOptions,
+      datetimeFrontMatterKey, datetimeFrontMatterValue, prettyDir
+    );
   }
 
   private @NotNull RenderOptions createRenderOptions(@NotNull ReplConfig replConfig) {
     var renderOptions = replConfig.literatePrettier.renderOptions;
     switch (prettyColor) {
       case emacs -> renderOptions.colorScheme = RenderOptions.ColorSchemeName.Emacs;
       case intellij -> renderOptions.colorScheme = RenderOptions.ColorSchemeName.IntelliJ;
-      case null -> {}
+      case null -> { }
     }
     return renderOptions;
   }

cli-console/src/main/java/org/aya/cli/console/MainArgs.java

@@ -81,6 +81,10 @@ public static class Action {
   public PrettyFormat prettyFormat;
   @Option(names = {"--pretty-dir"}, description = "Specify output directory of pretty printing.")
   public String prettyDir;
+  @Option(names = {"--datetime-front-matter-key"}, description = "If set, add datetime in the front matter using the value as YAML key.")
+  public String datetimeFrontMatterKey;
+  @Option(names = {"--datetime-front-matter"}, description = "Overwrites the datetime in the front matter.")
+  public String datetimeFrontMatterValue;
   @Option(names = {"--pretty-color"}, description = "The color theme of pretty printing." + CANDIDATES, defaultValue = "emacs")
   public PredefinedStyle prettyColor;
   @Option(names = {"--pretty-no-code-style"}, description = "Do not include default highlight styles.")

cli-impl/src/main/java/org/aya/cli/library/LibraryCompiler.java

@@ -13,6 +13,7 @@
 import org.aya.cli.single.CompilerFlags;
 import org.aya.cli.utils.CliEnums;
 import org.aya.cli.utils.CompilerUtil;
+import org.aya.cli.utils.LiterateData;
 import org.aya.generic.InterruptException;
 import org.aya.pretty.backend.string.StringPrinterConfig;
 import org.aya.pretty.printer.PrinterConfig;
@@ -171,6 +172,12 @@ private void pretty(ImmutableSeq<LibrarySource> modified) throws IOException {
     var litPretty = litConfig.pretty();
     var prettierOptions = litPretty != null ? litPretty.prettierOptions : cmdPretty.prettierOptions();
     var renderOptions = litPretty != null ? litPretty.renderOptions : cmdPretty.renderOptions();
+    var datetimeFMKey = cmdPretty.datetimeFrontMatterKey();
+    var datetimeFMValue = cmdPretty.datetimeFrontMatterValue();
+    if (datetimeFMKey == null) datetimeFMKey = litConfig.datetimeFrontMatterKey();
+    if (datetimeFMValue != null) datetimeFMKey = "date";
+    datetimeFMValue = StringUtil.timeInGitFormat();
+    var frontMatter = new LiterateData.InjectedFrontMatter(datetimeFMKey, datetimeFMValue);
     // always use the backend options from the command line, like output format, server-side rendering, etc.
     var outputTarget = cmdPretty.prettyFormat().target;
     var setup = cmdPretty.backendOpts(true).then(new RenderOptions.BackendSetup() {
@@ -187,7 +194,7 @@ private void pretty(ImmutableSeq<LibrarySource> modified) throws IOException {
     // THE BIG GAME
     modified.forEachChecked(src -> {
       // reportNest(STR."[Pretty] \{QualifiedID.join(src.moduleName())}");
-      var doc = src.pretty(ImmutableSeq.empty(), prettierOptions);
+      var doc = src.pretty(ImmutableSeq.empty(), frontMatter, prettierOptions);
       var text = renderOptions.render(outputTarget, doc, setup);
       var outputFileName = AyaFiles.stripAyaSourcePostfix(src.displayPath().toString()) + outputTarget.fileExt;
       var outputFile = outputDir.resolve(outputFileName);

cli-impl/src/main/java/org/aya/cli/library/json/LibraryConfig.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli.library.json;
 
@@ -27,8 +27,12 @@ public record LibraryConfig(
   @NotNull LibraryLiterateConfig literateConfig,
   @NotNull ImmutableSeq<LibraryDependency> deps
 ) {
+  /// @param datetimeFrontMatterKey it makes little sense to specify the "values" too,
+  ///                               because a library has many files, and each file should
+  ///                               have their own modified time, which is unrealistic to retrieve.
   public record LibraryLiterateConfig(
     @Nullable LiteratePrettierOptions pretty,
+    @Nullable String datetimeFrontMatterKey,
     @NotNull String linkPrefix,
     @NotNull Path outputPath
   ) {

cli-impl/src/main/java/org/aya/cli/library/json/LibraryConfigData.java

@@ -1,10 +1,11 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli.library.json;
 
 import com.google.gson.GsonBuilder;
 import com.google.gson.JsonParseException;
 import kala.collection.immutable.ImmutableSeq;
+import org.aya.cli.library.json.LibraryConfig.LibraryLiterateConfig;
 import org.aya.cli.utils.LiteratePrettierOptions;
 import org.aya.generic.Constants;
 import org.aya.prelude.GeneratedVersion;
@@ -38,16 +39,17 @@ public void checkDeserialization() {
       if (linkPrefix == null) linkPrefix = "/";
     }
 
-    public @NotNull LibraryConfig.LibraryLiterateConfig asConfig(@NotNull Path outputPath) {
+    public @NotNull LibraryLiterateConfig asConfig(@Nullable String datetimeFrontMatterKey, @NotNull Path outputPath) {
       checkDeserialization();
-      return new LibraryConfig.LibraryLiterateConfig(pretty, linkPrefix, outputPath);
+      return new LibraryLiterateConfig(pretty, datetimeFrontMatterKey, linkPrefix, outputPath);
     }
   }
 
   public String ayaVersion;
   public String name;
   public String group;
   public String version;
+  public String datetimeFrontMatterKey;
   public LibraryLiterateConfigData literate;
   public Map<String, LibraryDependencyData> dependency;
 
@@ -67,16 +69,15 @@ public void checkDeserialization() {
 
   private @NotNull LibraryConfig asConfig(
     @NotNull Path libraryRoot,
-    @Nullable LibraryConfig.LibraryLiterateConfig literateConfig,
+    @Nullable LibraryLiterateConfig literateConfig,
     @NotNull Function<String, Path> buildRootGen
   ) {
     checkDeserialization(libraryRoot.resolve(Constants.AYA_JSON));
     var buildRoot = FileUtil.canonicalize(buildRootGen.apply(version));
-    if (literateConfig == null) literateConfig = literate.asConfig(buildRoot.resolve("pretty"));
+    if (literateConfig == null) literateConfig = literate.asConfig(datetimeFrontMatterKey,
+      buildRoot.resolve("pretty"));
     return new LibraryConfig(
-      Version.create(ayaVersion),
-      name,
-      version,
+      Version.create(ayaVersion), name, version,
       libraryRoot,
       libraryRoot.resolve("src"),
       buildRoot,
@@ -109,7 +110,7 @@ public void checkDeserialization() {
 
   public static @NotNull LibraryConfig fromDependencyRoot(
     @NotNull Path dependencyRoot,
-    @Nullable LibraryConfig.LibraryLiterateConfig literateConfig,
+    @Nullable LibraryLiterateConfig literateConfig,
     @NotNull Function<String, Path> buildRoot
   ) throws IOException, BadConfig {
     var canonicalPath = FileUtil.canonicalize(dependencyRoot);

cli-impl/src/main/java/org/aya/cli/library/json/LibraryDependency.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang.
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli.library.json;
 
@@ -9,7 +9,7 @@
 public sealed interface LibraryDependency {
   @NotNull String depName();
 
-  record DepVersion(@NotNull String depName, @NotNull String version) implements LibraryDependency { }
-  record DepGithub(@NotNull String depName, @NotNull String repo) implements LibraryDependency { }
-  record DepFile(@NotNull String depName, @NotNull Path depRoot) implements LibraryDependency { }
+  record DepVersion(@Override @NotNull String depName, @NotNull String version) implements LibraryDependency { }
+  record DepGithub(@Override @NotNull String depName, @NotNull String repo) implements LibraryDependency { }
+  record DepFile(@Override @NotNull String depName, @NotNull Path depRoot) implements LibraryDependency { }
 }

cli-impl/src/main/java/org/aya/cli/library/source/LibrarySource.java

@@ -77,8 +77,12 @@ public void notifyTycked(@NotNull ResolveInfo moduleResolve, @NotNull ImmutableS
     }
   }
 
-  public @NotNull Doc pretty(@NotNull ImmutableSeq<Problem> problems, @NotNull PrettierOptions options) throws IOException {
-    return LiterateData.toDoc(this, moduleName(), program.get(), problems, options);
+  public @NotNull Doc pretty(
+    @NotNull ImmutableSeq<Problem> problems,
+    @NotNull LiterateData.InjectedFrontMatter frontMatter,
+    @NotNull PrettierOptions options
+  ) throws IOException {
+    return LiterateData.toDoc(this, moduleName(), program.get(), problems, frontMatter, options);
   }
 
   @Override public @NotNull ImmutableSeq<Stmt> parseMe(@NotNull GenericAyaParser parser) throws IOException {

cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java

@@ -32,10 +32,11 @@ public record CompilerFlags(
       CliEnums.detectFormat(outputFile),
       AyaPrettierOptions.pretty(),
       renderOptions,
-      null);
+      null, null, null);
     return null;
   }
 
+  /// @param datetimeFrontMatterValue see {@link org.aya.cli.utils.LiterateData.InjectedFrontMatter}
   public record PrettyInfo(
     boolean ascii,
     boolean prettyNoCodeStyle,
@@ -45,6 +46,8 @@ public record PrettyInfo(
     @NotNull CliEnums.PrettyFormat prettyFormat,
     @NotNull PrettierOptions prettierOptions,
     @NotNull RenderOptions renderOptions,
+    @Nullable String datetimeFrontMatterKey,
+    @Nullable String datetimeFrontMatterValue,
     @Nullable String prettyDir
   ) {
     public @NotNull RenderOptions.DefaultSetup backendOpts(boolean headerCode) {

cli-impl/src/main/java/org/aya/cli/single/SingleAyaFile.java

@@ -22,6 +22,7 @@
 import org.aya.util.FileUtil;
 import org.aya.util.error.SourceFile;
 import org.aya.util.error.SourceFileLocator;
+import org.aya.util.more.StringUtil;
 import org.aya.util.prettier.PrettierOptions;
 import org.aya.util.reporter.CollectingReporter;
 import org.aya.util.reporter.Problem;
@@ -64,7 +65,11 @@ public sealed interface SingleAyaFile extends GenericAyaFile {
 
     var renderOptions = flags.renderOptions();
     if (currentStage == CliEnums.PrettyStage.literate) {
-      var d = toDoc((ImmutableSeq<Stmt>) doc, reporter.problems().toImmutableSeq(), flags.prettierOptions());
+      var value = flags.datetimeFrontMatterValue();
+      if (value == null) value = StringUtil.timeInGitFormat();
+      var frontMatter = new LiterateData.InjectedFrontMatter(flags.datetimeFrontMatterKey(), value);
+      var d = toDoc((ImmutableSeq<Stmt>) doc, reporter.problems().toImmutableSeq(),
+        frontMatter, flags.prettierOptions());
       var text = renderOptions.render(out, d, flags.backendOpts(true));
       FileUtil.writeString(prettyDir.resolve(fileName), text);
     } else {
@@ -75,9 +80,9 @@ public sealed interface SingleAyaFile extends GenericAyaFile {
   @VisibleForTesting default @NotNull Doc toDoc(
     @NotNull ImmutableSeq<Stmt> program,
     @NotNull ImmutableSeq<Problem> problems,
-    @NotNull PrettierOptions options
+    @NotNull LiterateData.InjectedFrontMatter frontMatter, @NotNull PrettierOptions options
   ) throws IOException {
-    return LiterateData.toDoc(this, null, program, problems, options);
+    return LiterateData.toDoc(this, null, program, problems, frontMatter, options);
   }
 
   private void doWrite(

cli-impl/src/main/java/org/aya/cli/utils/LiterateData.java

@@ -4,6 +4,7 @@
 
 import kala.collection.Seq;
 import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableList;
 import kala.control.Option;
 import org.aya.cli.literate.AyaMdParser;
 import org.aya.cli.literate.LiterateFaithfulPrettier;
@@ -102,15 +103,35 @@ public void tyck(@NotNull ResolveInfo info) {
     });
   }
 
+  public record InjectedFrontMatter(
+    @Nullable String datetimeKey,
+    @NotNull String datetimeValue
+  ) { }
   public static @NotNull Doc toDoc(
     @NotNull GenericAyaFile ayaFile,
     @Nullable ModulePath currentFileModule,
     @NotNull ImmutableSeq<Stmt> program,
     @NotNull ImmutableSeq<Problem> problems,
+    @NotNull InjectedFrontMatter injected,
     @NotNull PrettierOptions options
   ) throws IOException {
     var highlights = SyntaxHighlight.highlight(currentFileModule, Option.some(ayaFile.codeFile()), program);
     var literate = ayaFile.literate();
+    if (injected.datetimeKey != null) {
+      var frontMatter = literate.findFrontMatter();
+      var label = new Literate.Raw(Doc.plain(injected.datetimeKey + ": " + injected.datetimeValue));
+      if (frontMatter != null) {
+        // They must be non-empty because the front matter starts with a ---
+        var secondLast = frontMatter.children().size() - 2;
+        frontMatter.children().insert(secondLast, label);
+        frontMatter.children().insert(secondLast, Literate.EOL);
+      } else {
+        var delimiter = new Literate.Raw(Doc.plain("---"));
+        frontMatter = new Literate.FrontMatter(MutableList.of(
+          delimiter, Literate.EOL, label, Literate.EOL, delimiter));
+        literate = new Literate.Many(null, ImmutableSeq.of(frontMatter, literate));
+      }
+    }
     var prettier = new LiterateFaithfulPrettier(problems, highlights, options);
     prettier.accept(literate);
     return literate.toDoc();

cli-impl/src/test/java/org/aya/test/LibraryTest.java

@@ -73,7 +73,7 @@ public static void main(String... args) throws IOException {
   private static @NotNull CompilerFlags makeFlagsForPretty() {
     var prettyInfo = new CompilerFlags.PrettyInfo(
       true, false, false, false, CliEnums.PrettyStage.literate,
-      CliEnums.PrettyFormat.html, AyaPrettierOptions.pretty(), new RenderOptions(), null
+      CliEnums.PrettyFormat.html, AyaPrettierOptions.pretty(), new RenderOptions(), null, null, null
     );
     return new CompilerFlags(CompilerFlags.Message.ASCII, false, false, prettyInfo, SeqView.empty(), null);
   }

cli-impl/src/test/java/org/aya/test/cli/LibraryGraphTest.java

@@ -52,7 +52,7 @@ public TestLibraryOwner(@NotNull LibraryConfig underlyingLibrary) {
       libRoot.resolve("src"),
       libRoot.resolve("build"),
       libRoot.resolve("build/out"),
-      new LibraryConfig.LibraryLiterateConfig(new LiteratePrettierOptions(), "11.4.5.14", libRoot.resolve("literate")),
+      new LibraryConfig.LibraryLiterateConfig(new LiteratePrettierOptions(), null, "11.4.5.14", libRoot.resolve("literate")),
       ImmutableSeq.empty()
     );
   }