literate: allow user specified datetime, so we can pass in the git da…

…tetime

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

@@ -121,7 +121,7 @@ private int doCompile(@NotNull CompileAction compile) throws IOException {
       prettyStage,
       prettyFormat,
       prettierOptions, renderOptions,
-      datetimeFrontMatterKey, prettyDir
+      datetimeFrontMatterKey, datetimeFrontMatterValue, prettyDir
     );
   }
 

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

@@ -83,6 +83,8 @@ public static class Action {
   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,9 +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 datetimeFrontMatterKey = cmdPretty.datetimeFrontMatterKey() != null
-      ? cmdPretty.datetimeFrontMatterKey()
-      : litConfig.datetimeFrontMatterKey();
+    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() {
@@ -190,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(), datetimeFrontMatterKey, 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/source/LibrarySource.java

@@ -22,7 +22,6 @@
 import org.aya.util.reporter.Problem;
 import org.jetbrains.annotations.Debug;
 import org.jetbrains.annotations.NotNull;
-import org.jetbrains.annotations.Nullable;
 
 import java.io.IOException;
 import java.nio.file.Files;
@@ -80,10 +79,10 @@ public void notifyTycked(@NotNull ResolveInfo moduleResolve, @NotNull ImmutableS
 
   public @NotNull Doc pretty(
     @NotNull ImmutableSeq<Problem> problems,
-    @Nullable String datetimeFrontMatterKey,
+    @NotNull LiterateData.InjectedFrontMatter frontMatter,
     @NotNull PrettierOptions options
   ) throws IOException {
-    return LiterateData.toDoc(this, moduleName(), program.get(), problems, datetimeFrontMatterKey, options);
+    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, null);
     return null;
   }
 
+  /// @param datetimeFrontMatterValue see {@link org.aya.cli.utils.LiterateData.InjectedFrontMatter}
   public record PrettyInfo(
     boolean ascii,
     boolean prettyNoCodeStyle,
@@ -46,6 +47,7 @@ public record PrettyInfo(
     @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,8 +65,11 @@ public sealed interface SingleAyaFile extends GenericAyaFile {
 
     var renderOptions = flags.renderOptions();
     if (currentStage == CliEnums.PrettyStage.literate) {
+      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(),
-        flags.datetimeFrontMatterKey(), flags.prettierOptions());
+        frontMatter, flags.prettierOptions());
       var text = renderOptions.render(out, d, flags.backendOpts(true));
       FileUtil.writeString(prettyDir.resolve(fileName), text);
     } else {
@@ -76,9 +80,9 @@ public sealed interface SingleAyaFile extends GenericAyaFile {
   @VisibleForTesting default @NotNull Doc toDoc(
     @NotNull ImmutableSeq<Stmt> program,
     @NotNull ImmutableSeq<Problem> problems,
-    @Nullable String datetimeFrontMatterKey, @NotNull PrettierOptions options
+    @NotNull LiterateData.InjectedFrontMatter frontMatter, @NotNull PrettierOptions options
   ) throws IOException {
-    return LiterateData.toDoc(this, null, program, problems, datetimeFrontMatterKey, options);
+    return LiterateData.toDoc(this, null, program, problems, frontMatter, options);
   }
 
   private void doWrite(

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

@@ -37,8 +37,6 @@
 import org.jetbrains.annotations.Nullable;
 
 import java.io.IOException;
-import java.time.ZonedDateTime;
-import java.time.format.DateTimeFormatter;
 
 public record LiterateData(
   @NotNull Literate literate,
@@ -105,20 +103,23 @@ 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,
-    @Nullable String datetimeFrontMatterKey,
+    @NotNull InjectedFrontMatter injected,
     @NotNull PrettierOptions options
   ) throws IOException {
     var highlights = SyntaxHighlight.highlight(currentFileModule, Option.some(ayaFile.codeFile()), program);
     var literate = ayaFile.literate();
-    if (datetimeFrontMatterKey != null) {
-      var datetime = ZonedDateTime.now().format(DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss X"));
+    if (injected.datetimeKey != null) {
       var frontMatter = literate.findFrontMatter();
-      var label = new Literate.Raw(Doc.plain(datetimeFrontMatterKey + ": " + datetime));
+      var label = new Literate.Raw(Doc.plain(injected.datetimeKey + ": " + injected.datetimeValue));
       if (frontMatter != null) {
         frontMatter.children().append(label);
       } else {

cli-impl/src/test/java/org/aya/test/literate/AyaMdParserTest.java

@@ -7,6 +7,7 @@
 import org.aya.cli.single.CompilerFlags;
 import org.aya.cli.single.SingleAyaFile;
 import org.aya.cli.single.SingleFileCompiler;
+import org.aya.cli.utils.LiterateData;
 import org.aya.generic.Constants;
 import org.aya.prettier.AyaPrettierOptions;
 import org.aya.primitive.PrimFactory;
@@ -17,6 +18,7 @@
 import org.aya.util.FileUtil;
 import org.aya.util.error.Global;
 import org.aya.util.error.SourceFile;
+import org.aya.util.more.StringUtil;
 import org.aya.util.reporter.BufferReporter;
 import org.aya.util.reporter.IgnoringReporter;
 import org.aya.util.reporter.ThrowingReporter;
@@ -97,8 +99,9 @@ public void testHighlight(String caseName) throws IOException {
     loader.tyckModule(info, null);
     literate.tyckAdditional(info);
 
+    var defaultFM = new LiterateData.InjectedFrontMatter(null, StringUtil.timeInGitFormat());
     var doc = literate.toDoc(stmts, reporter.problems().toImmutableSeq(),
-      null, AyaPrettierOptions.pretty()).toDoc();
+      defaultFM, AyaPrettierOptions.pretty()).toDoc();
     reporter.problems().clear();
     // save some coverage
     var actualTexInlinedStyle = doc.renderToTeX();

tools-kala/src/main/java/org/aya/util/more/StringUtil.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.util.more;
 
@@ -7,6 +7,9 @@
 import kala.tuple.primitive.IntObjTuple2;
 import org.jetbrains.annotations.NotNull;
 
+import java.time.ZonedDateTime;
+import java.time.format.DateTimeFormatter;
+
 public interface StringUtil {
   /** <a href="https://github.com/JetBrains/Arend/blob/39b14869ac5abdcee7bbee0efa06d5a6f86c4069/cli/src/main/java/org/arend/frontend/library/TimedLibraryManager.java#L21-L31">Arend</a> */
   static @NotNull String timeToString(long time) {
@@ -16,6 +19,10 @@ public interface StringUtil {
     return (seconds / 60) + "m" + (seconds % 60) + "s";
   }
 
+  static @NotNull String timeInGitFormat() {
+    return ZonedDateTime.now().format(DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss X"));
+  }
+
   /**
    * all line separators are treat as 1 character long
    *