diff --git a/eo-phi-normalizer/app/Main.hs b/eo-phi-normalizer/app/Main.hs index 333c150e..24eb6081 100644 --- a/eo-phi-normalizer/app/Main.hs +++ b/eo-phi-normalizer/app/Main.hs @@ -53,6 +53,7 @@ import Language.EO.Phi.Report.Data (makeProgramReport, makeReport) import Language.EO.Phi.Report.Html (reportCSS, reportJS, toStringReport) import Language.EO.Phi.Rules.Common import Language.EO.Phi.Rules.Fast (fastYegorInsideOut, fastYegorInsideOutAsRule) +import Language.EO.Phi.Rules.RunYegor (yegorRuleSet) import Language.EO.Phi.Rules.Yaml (RuleSet (rules, title), convertRuleNamed, parseRuleSetFromFile) import Language.EO.Phi.ToLaTeX import Main.Utf8 @@ -100,6 +101,13 @@ data CLI'MetricsPhi = CLI'MetricsPhi } deriving stock (Show) +data CLI'PrintRules = CLI'PrintRules + { rulesPath :: Maybe String + , latex :: Bool + , compact :: Bool + } + deriving stock (Show) + newtype CLI'Pipeline'Report = CLI'Pipeline'Report { configFile :: FilePath } @@ -127,6 +135,7 @@ data CLI = CLI'TransformPhi' CLI'TransformPhi | CLI'DataizePhi' CLI'DataizePhi | CLI'MetricsPhi' CLI'MetricsPhi + | CLI'PrintRules' CLI'PrintRules | CLI'Pipeline' CLI'Pipeline deriving stock (Show) @@ -189,6 +198,9 @@ jsonSwitch = switch (long "json" <> short 'j' <> help "Output JSON.") latexSwitch :: Parser Bool latexSwitch = switch (long "tex" <> help "Output LaTeX.") +compactSwitch :: Parser Bool +compactSwitch = switch (long "compact" <> short 'c' <> help "Print rules, each on a single line.") + asPackageSwitch :: Parser Bool asPackageSwitch = switch (long "as-package" <> help "Automatically inject (λ → Package) in the program if necessary, to dataize all fields.") @@ -223,6 +235,7 @@ data CommandParser = CommandParser , dataize :: Parser CLI'DataizePhi , pipeline :: Parser CLI'Pipeline , pipeline' :: CommandParser'Pipeline + , printRules :: Parser CLI'PrintRules } commandParser :: CommandParser @@ -234,7 +247,11 @@ commandParser = outputFile <- outputFileOption bindingsPath <- bindingsPathOption pure CLI'MetricsPhi{..} - + printRules = do + rulesPath <- optional $ strOption (long "rules" <> short 'r' <> metavar.file <> help [fmt|{metavarName.file} with user-defined rules. If unspecified, yegor.yaml is rendered.|]) + latex <- latexSwitch + compact <- compactSwitch + pure CLI'PrintRules{..} transform = do rulesPath <- optional $ strOption (long "rules" <> short 'r' <> metavar.file <> help [fmt|{metavarName.file} with user-defined rules. If unspecified, builtin set of rules is used.|]) chain <- switch (long "chain" <> short 'c' <> help "Output transformation steps.") @@ -296,6 +313,7 @@ data CommandParserInfo = CommandParserInfo { metrics :: ParserInfo CLI , transform :: ParserInfo CLI , dataize :: ParserInfo CLI + , printRules :: ParserInfo CLI , pipeline :: ParserInfo CLI , pipeline' :: CommandParserInfo'Pipeline } @@ -306,6 +324,7 @@ commandParserInfo = { metrics = info (CLI'MetricsPhi' <$> commandParser.metrics) (progDesc "Collect metrics for a PHI program.") , transform = info (CLI'TransformPhi' <$> commandParser.transform) (progDesc "Transform a PHI program.") , dataize = info (CLI'DataizePhi' <$> commandParser.dataize) (progDesc "Dataize a PHI program.") + , printRules = info (CLI'PrintRules' <$> commandParser.printRules) (progDesc "Print rules in LaTeX format.") , pipeline = info (CLI'Pipeline' <$> commandParser.pipeline) (progDesc "Run pipeline-related commands.") , pipeline' = CommandParserInfo'Pipeline @@ -325,6 +344,7 @@ data CommandNames = CommandNames { transform :: String , metrics :: String , dataize :: String + , printRules :: String , pipeline :: String , pipeline' :: CommandNames'Pipeline } @@ -335,6 +355,7 @@ commandNames = { transform = "transform" , metrics = "metrics" , dataize = "dataize" + , printRules = "print-rules" , pipeline = "pipeline" , pipeline' = CommandNames'Pipeline @@ -351,6 +372,7 @@ cli = <> command commandNames.metrics commandParserInfo.metrics <> command commandNames.dataize commandParserInfo.dataize <> command commandNames.pipeline commandParserInfo.pipeline + <> command commandNames.printRules commandParserInfo.printRules ) cliOpts :: ParserInfo CLI @@ -508,6 +530,11 @@ main = withUtf8 do -- logStrLn "Computing metrics" metrics <- getMetrics bindingsPath inputFile logStrLn $ encodeToJSONString metrics + CLI'PrintRules' CLI'PrintRules{..} -> do + (logStrLn, _) <- getLoggers Nothing + rules <- rules <$> maybe (return yegorRuleSet) parseRuleSetFromFile rulesPath + let toLatex' = if compact then rulesToLatexCompact else toLatex + logStrLn $ show $ toLatex' rules CLI'TransformPhi' CLI'TransformPhi{..} -> do program' <- getProgram inputFile deps <- mapM (getProgram . Just) dependencies diff --git a/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs b/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs index 7c94b06e..6e6a7e86 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs @@ -1,6 +1,8 @@ {-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} module Language.EO.Phi.ToLaTeX where @@ -9,6 +11,7 @@ import Data.List (intersperse) import Data.String (IsString) import Data.Text qualified as T import Language.EO.Phi +import Language.EO.Phi.Rules.Yaml import Text.Regex (mkRegex, subRegex) newtype LaTeX = LaTeX {unLaTeX :: String} @@ -31,7 +34,7 @@ instance ToLatex Attribute where toLatex Rho = "^" toLatex (Alpha (AlphaIndex a)) = LaTeX ("\\alpha_" ++ tail a) toLatex (Label (LabelId l)) = LaTeX l - toLatex (MetaAttr _) = error "rendering MetaBindings in LaTex format" + toLatex (MetaAttr (LabelMetaId l)) = LaTeX l instance ToLatex Binding where toLatex (AlphaBinding attr obj) = toLatex attr <> " -> " <> toLatex obj @@ -39,8 +42,8 @@ instance ToLatex Binding where toLatex (DeltaBinding (Bytes bytes)) = "D> " <> LaTeX bytes toLatex DeltaEmptyBinding = "D> ?" toLatex (LambdaBinding (Function fn)) = "L> " <> LaTeX fn - toLatex (MetaBindings _) = error "rendering MetaBindings in LaTex format" - toLatex (MetaDeltaBinding _) = error "rendering MetaDeltaBinding in LaTex format" + toLatex (MetaBindings (BindingsMetaId x)) = LaTeX x + toLatex (MetaDeltaBinding (BytesMetaId x)) = "D> " <> LaTeX x instance ToLatex Object where toLatex (Formation bindings) = @@ -50,20 +53,99 @@ instance ToLatex Object where toLatex (ObjectDispatch obj attr) = toLatex obj <> "." <> toLatex attr toLatex GlobalObject = "Q" - toLatex ThisObject = "$" + toLatex ThisObject = "\\xi" toLatex Termination = "\\dead" - toLatex (MetaObject _) = error "rendering MetaObject in LaTex format" + toLatex (MetaObject (ObjectMetaId metaId)) = LaTeX metaId toLatex MetaTailContext{} = error "rendering MetaTailContext in LaTex format" toLatex (MetaFunction _ _) = error "rendering MetaFunction in LaTex format" - toLatex (MetaSubstThis _ _) = error "rendering MetaSubstThis in LaTex format" + toLatex (MetaSubstThis obj1 obj2) = LaTeX "\\mathbb{S}(" <> toLatex obj1 <> ", " <> toLatex obj2 <> ")" removeOrgEolang :: String -> String removeOrgEolang = T.unpack . T.replace "Q.org.eolang" "QQ" . T.pack +substituteTau :: String -> String +substituteTau = T.unpack . T.replace "τ" "\\tau" . T.pack + +removeExclamationsMarks :: String -> String +removeExclamationsMarks = filter (/= '!') + removeAlpha :: String -> String removeAlpha s = subRegex (mkRegex "\\\\alpha_([0-9]+) ->") s "\\1->" -- >>> toLatex ("{ ⟦ α0 ↦ ξ, α1 ↦ Φ.org.eolang.bytes( Δ ⤍ 00- ) ⟧ }" :: Program) -- \Big\{ [[ 0-> $, 1-> QQ.bytes( D> 00- ) ]] \Big\} latexToString :: LaTeX -> String -latexToString = removeAlpha . removeOrgEolang . unLaTeX +latexToString = removeExclamationsMarks . substituteTau . removeAlpha . removeOrgEolang . unLaTeX + +inMathMode :: LaTeX -> LaTeX +inMathMode = (" $ " <>) . (<> " $ ") + +-- it's ok without separators here because rules have zero or one constraint from the context +instance ToLatex RuleContext where + toLatex RuleContext{..} = + maybe mempty (\x -> inMathMode $ toLatex GlobalObject <> " -> " <> toLatex x) global_object + <> maybe mempty (\x -> (inMathMode $ toLatex x) <> " is the scope of the redex") current_object + <> maybe mempty (\x -> toLatex x <> " is the current attribute") current_attribute + +instance ToLatex RuleAttribute where + toLatex (ObjectAttr a) = toLatex a + toLatex DeltaAttr = "\\Delta" + toLatex LambdaAttr = "\\lambda" + +instance ToLatex Condition where + toLatex (IsNF nf) = inMathMode $ toLatex nf <> "\\in\\mathcal{N}" + toLatex (IsNFInsideFormation nf_inside_formation) = + (inMathMode $ toLatex nf_inside_formation) <> " is nf inside formation" + toLatex (PresentAttrs (AttrsInBindings attrs bindings)) = + inMathMode $ fold (intersperse ", " (map toLatex attrs)) <> " \\in " <> foldMap toLatex bindings + toLatex (AbsentAttrs (AttrsInBindings attrs bindings)) = + inMathMode $ fold (intersperse ", " (map toLatex attrs)) <> " \\notin " <> foldMap toLatex bindings + toLatex (AttrNotEqual (attr1, attr2)) = + inMathMode $ toLatex attr1 <> " \\neq " <> toLatex attr2 + toLatex (ApplyInSubformations apply_in_subformations) = + if not apply_in_subformations then LaTeX "not in subformations" else mempty + toLatex (ApplyInAbstractSubformations apply_in_abstract_subformations) = + if not apply_in_abstract_subformations then LaTeX "not in subformations" else mempty + +isNonEmptyContext :: Maybe RuleContext -> Bool +isNonEmptyContext Nothing = False +isNonEmptyContext (Just (RuleContext Nothing Nothing Nothing)) = False +isNonEmptyContext _ = True + +-- Renders all conditions on separate lines +instance ToLatex Rule where + toLatex (Rule name _ context _ pattern result _ when _) = + "\\rrule{" + <> LaTeX name + <> "}: &" + <> inMathMode (toLatex pattern) + <> "\\(\\trans\\)" + <> inMathMode (toLatex result) + <> (if not (null when) || isNonEmptyContext context then "\\\\\\text {if }" else mempty) + <> maybe mempty (\c -> "&" <> toLatex c <> "\\\\") context + <> fold (intersperse ",\\\\" (map (("&" <>) . toLatex) when)) + +instance ToLatex [Rule] where + toLatex rules = + "\\begin{figure*}\n\\begin{tabular}{rl}\n " + <> fold (intersperse "\\\\\\\\\n " (map toLatex rules)) + <> "\n\\end{tabular}\n\\end{figure*}" + +-- Renders all conditions in one line +ruleToLatexCompact :: Rule -> LaTeX +ruleToLatexCompact (Rule name _ context _ pattern result _ when _) = + "\\rrule{" + <> LaTeX name + <> "}: " + <> inMathMode (toLatex pattern) + <> "\\(\\trans\\)" + <> inMathMode (toLatex result) + <> (if not (null when) || isNonEmptyContext context then "\\quad\\text {if }" else "") + <> maybe mempty (\c -> toLatex c <> ", ") context + <> fold (intersperse ", " (map toLatex when)) + +rulesToLatexCompact :: [Rule] -> LaTeX +rulesToLatexCompact rules = + "\\begin{figure*}\n " + <> fold (intersperse "\\\\\\vspace*{0.5em}\n " (map ruleToLatexCompact rules)) + <> "\n\\end{figure*}" diff --git a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml index 26099088..76913f40 100644 --- a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml +++ b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml @@ -1,30 +1,7 @@ title: "Rule set based on Yegor's draft" rules: - # - name: Rule 3 - # description: 'Initialization of parent attribute' - # pattern: | - # ⟦ !B ⟧ - # result: | - # ⟦ !B, ρ ↦ ξ.σ ⟧ - # when: - # - present_attrs: - # attrs: ['σ'] - # bindings: ['!B'] - # - absent_attrs: - # attrs: ['ρ'] - # bindings: ['!B'] - # tests: - # - name: 'Has sigma and no rho' - # input: '⟦ b ↦ ⟦ ⟧, σ ↦ ⟦ ⟧ ⟧ ' - # output: ['⟦ b ↦ ⟦ ⟧, σ ↦ ⟦ ⟧, ρ ↦ ξ.σ ⟧'] - # - name: 'Has both sigma and rho' - # input: '⟦ a ↦ ⟦ b ↦ ⟦ ⟧, ρ ↦ ⟦ ⟧, σ ↦ ⟦ ⟧ ⟧ ⟧' - # output: [] - # - name: 'Has neither sigma nor rho' - # input: '⟦ a ↦ ⟦ b ↦ ⟦ ⟧ ⟧ ⟧' - # output: [] - - name: Φ-dispatch + - name: Phi description: 'Φ-dispatch' context: global_object: '!b' @@ -36,7 +13,7 @@ rules: - apply_in_subformations: false tests: [] - - name: ξ-dispatch + - name: xi description: 'ξ-dispatch' context: current_object: '!b' @@ -46,16 +23,13 @@ rules: !b when: - apply_in_subformations: false - # - present_attrs: - # attrs: ['ρ'] - # bindings: ['!B'] tests: - name: Does not replace ξ inside a subformation input: '⟦ a ↦ ⟦ ⟧, x ↦ ξ.a, ρ ↦ ⟦ ⟧ ⟧' output: [] # How to test replacing without already having context? - - name: R_DOT + - name: DOT description: 'Accessing an α-binding' pattern: | ⟦ !τ ↦ !b, !B ⟧.!τ @@ -82,22 +56,8 @@ rules: - name: Should respect surrounding context input: ⟦ hello ↦ ⟦⟧, goodbye ↦ ⟦ a ↦ ⟦⟧ ⟧ ⟧.hello output: ['⟦ ρ ↦ ⟦ hello ↦ ⟦⟧, goodbye ↦ ⟦ a ↦ ⟦⟧ ⟧ ⟧ ⟧'] - # - name: Rule 6a - # description: 'Accessing an α-binding (for object with ρ ↦ ∅)' - # pattern: | - # ⟦ !τ ↦ !b, ρ ↦ ∅, !B ⟧.!τ - # result: | - # !b[ ξ ↦ ⟦ !τ ↦ !b, ρ ↦ ∅, !B ⟧ ] - # when: [] - # tests: - # - name: Should match - # input: ⟦ hello ↦ ⟦⟧, ρ ↦ ∅ ⟧.hello - # output: ['⟦ ρ ↦ ⟦ hello ↦ ⟦⟧, ρ ↦ ∅ ⟧ ⟧'] - # - name: Shouldn't match - # input: ⟦ ⟧.hello - # output: [] - - name: R_DOT_ρ + - name: DOTrho description: 'Accessing ρ-binding' pattern: | ⟦ ρ ↦ !b, !B ⟧.ρ @@ -110,42 +70,63 @@ rules: input: ⟦ ρ ↦ ⟦ ⟧ ⟧.ρ output: ['⟦ ⟧'] - - name: R_COPY2 + - name: phi + description: 'Accessing a decorated object' + pattern: | + ⟦!B ⟧.!τ + result: | + ⟦!B ⟧.φ.!τ + when: + - present_attrs: + attrs: ['φ'] + bindings: ['!B'] + - absent_attrs: + attrs: ['!τ'] + bindings: ['!B'] + tests: + - name: 'Attribute does not exist' + input: '⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.b' + output: ['⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.φ.b'] + - name: 'Attribute exists' + input: '⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.a' + output: [] + - name: 'Both attributes do not exist' + input: '⟦ b ↦ ⟦⟧ ⟧.a' + output: [] + + - name: COPY description: 'Application of α-binding' - # Warning: this is not correct for the chain variant because it only matches the first two bindings - # i.e., doesn't match an empty binding after an attached one. - # We should instead match the first two empty bindings. context: - current_object: "!b_cur" + current_object: "!b2" pattern: | - ⟦ !τ1 ↦ ∅, !τ2 ↦ ∅, !B ⟧(α0 ↦ !b0, α1 ↦ !b1) + ⟦ !τ ↦ ∅, !B1 ⟧(!τ ↦ !b1, !B2) result: | - ⟦ !τ1 ↦ !b0[ ξ ↦ !b_cur ], !τ2 ↦ !b1[ ξ ↦ !b_cur ], !B ⟧ + ⟦ !τ ↦ !b1[ ξ ↦ !b2 ], !B1 ⟧(!B2) when: - apply_in_subformations: false - - nf: '!b0' - nf: '!b1' tests: - - name: Should match positional arguments - input: ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧) - output: ['⟦ hello ↦ ⟦ ρ ↦ ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧) ⟧, bye ↦ ⟦ a ↦ ⟦⟧, ρ ↦ ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧) ⟧, hey ↦ ∅ ⟧'] - options: - - take_one: true + - name: Should match + input: ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧) + output: ['⟦ a ↦ ⟦ ρ ↦ ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧) ⟧ ⟧()'] + - name: Should not match in subformations + input: ⟦ a ↦ ⟦b ↦ ∅⟧(b ↦ ⟦⟧) ⟧ + output: [] - - name: R_COPY1 + - name: COPY1 description: 'Application of α-binding' # Warning: this is not correct for the chain variant because it only matches the first binding # i.e., doesn't match an empty binding after an attached one. # We should instead match the first empty binding. context: - current_object: "!b_cur" + current_object: "!b2" pattern: | - ⟦ !τ ↦ ∅, !B ⟧(α0 ↦ !b) + ⟦ !τ ↦ ∅, !B ⟧(α0 ↦ !b1) result: | - ⟦ !τ ↦ !b[ ξ ↦ !b_cur ], !B ⟧ + ⟦ !τ ↦ !b1[ ξ ↦ !b2 ], !B ⟧ when: - apply_in_subformations: false - - nf: '!b' + - nf: '!b1' tests: - name: Should match first void attribute input: ⟦ hello ↦ ⟦⟧, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧) @@ -153,26 +134,39 @@ rules: options: - take_one: true - - name: R_COPY + - name: COPY2 description: 'Application of α-binding' + # Warning: this is not correct for the chain variant because it only matches the first two bindings + # i.e., doesn't match an empty binding after an attached one. + # We should instead match the first two empty bindings. context: - current_object: "!b_cur" + current_object: "!b3" pattern: | - ⟦ !τ ↦ ∅, !B1 ⟧(!τ ↦ !b, !B2) + ⟦ !τ1 ↦ ∅, !τ2 ↦ ∅, !B ⟧(α0 ↦ !b1, α1 ↦ !b2) result: | - ⟦ !τ ↦ !b[ ξ ↦ !b_cur ], !B1 ⟧(!B2) + ⟦ !τ1 ↦ !b1[ ξ ↦ !b3 ], !τ2 ↦ !b2[ ξ ↦ !b3 ], !B ⟧ when: - apply_in_subformations: false - - nf: '!b' + - nf: '!b1' + - nf: '!b2' tests: - - name: Should match - input: ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧) - output: ['⟦ a ↦ ⟦ ρ ↦ ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧) ⟧ ⟧()'] - - name: Should not match in subformations - input: ⟦ a ↦ ⟦b ↦ ∅⟧(b ↦ ⟦⟧) ⟧ - output: [] + - name: Should match positional arguments + input: ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧) + output: ['⟦ hello ↦ ⟦ ρ ↦ ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧) ⟧, bye ↦ ⟦ a ↦ ⟦⟧, ρ ↦ ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧) ⟧, hey ↦ ∅ ⟧'] + options: + - take_one: true + + - name: COPYdelta + description: 'Application of Δ-binding' + pattern: | + ⟦ Δ ⤍ ∅, !B ⟧(Δ ⤍ !y) + result: | + ⟦ Δ ⤍ !y, !B ⟧ + when: + - apply_in_abstract_subformations: false + tests: [] - - name: R_COPY_EMPTY + - name: EMPTY description: 'Empty application' pattern: | ⟦ !B1 ⟧() @@ -193,41 +187,7 @@ rules: input: ⟦⟧() output: ['⟦⟧'] - - name: R_COPY_Δ - description: 'Application of Δ-binding' - pattern: | - ⟦ Δ ⤍ ∅, !B ⟧(Δ ⤍ !y) - result: | - ⟦ Δ ⤍ !y, !B ⟧ - when: - - apply_in_abstract_subformations: false - tests: [] - - - name: R_φ - description: 'Accessing a decorated object' - pattern: | - ⟦!B ⟧.!τ - result: | - ⟦!B ⟧.φ.!τ - when: - - present_attrs: - attrs: ['φ'] - bindings: ['!B'] - - absent_attrs: - attrs: ['!τ'] - bindings: ['!B'] - tests: - - name: 'Attribute does not exist' - input: '⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.b' - output: ['⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.φ.b'] - - name: 'Attribute exists' - input: '⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.a' - output: [] - - name: 'Both attributes do not exist' - input: '⟦ b ↦ ⟦⟧ ⟧.a' - output: [] - - - name: R_OVER + - name: OVER description: 'Invalid application (attribute already attached)' pattern: ⟦ !τ ↦ !b1, !B1 ⟧(!τ ↦ !b2, !B2) result: ⊥ @@ -237,9 +197,28 @@ rules: input: '⟦ t ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)' output: ['⊥'] - - name: R_MISS + - name: STOP + description: 'Invalid attribute access' + pattern: | + ⟦ !B ⟧.!τ + result: | + ⊥ + when: + - absent_attrs: + attrs: ['!τ', 'φ', 'λ'] + bindings: ['!B'] + - present_attrs: + attrs: ['ρ'] + bindings: ['!B'] + - nf: '⟦ !B ⟧' + tests: + - name: 'Accessing nonexistent attribute' + input: '⟦ ρ ↦ ⟦ ⟧ ⟧.x' + output: ['⊥'] + + - name: MISS description: 'Invalid application (absent attribute)' - pattern: ⟦ !B1 ⟧(!τ ↦ !b2, !B2) + pattern: ⟦ !B1 ⟧(!τ ↦ !b, !B2) result: ⊥ when: - absent_attrs: @@ -259,26 +238,7 @@ rules: input: ⟦ a ↦ ⟦ b ↦ ⟦⟧(t ↦ ⟦⟧) ⟧ ⟧ output: ['⟦ a ↦ ⟦ b ↦ ⊥ ⟧ ⟧'] - - name: R_STOP - description: 'Invalid attribute access' - pattern: | - ⟦ !B ⟧.!τ - result: | - ⊥ - when: - - absent_attrs: - attrs: ['!τ', 'φ', 'λ'] - bindings: ['!B'] - - present_attrs: - attrs: ['ρ'] - bindings: ['!B'] - - nf: '⟦ !B ⟧' - tests: - - name: 'Accessing nonexistent attribute' - input: '⟦ ρ ↦ ⟦ ⟧ ⟧.x' - output: ['⊥'] - - - name: R_DD + - name: DD description: 'Accessing an attribute on bottom' pattern: | ⊥.!τ @@ -293,7 +253,7 @@ rules: input: '⟦ ⟧.a' output: [] - - name: R_DC + - name: DC description: 'Application on bottom is bottom' pattern: | ⊥(!B) diff --git a/flake.nix b/flake.nix index 7db0bf2c..ce0d256d 100644 --- a/flake.nix +++ b/flake.nix @@ -209,6 +209,7 @@ "normalizer/dataize.md" "normalizer/metrics.md" "normalizer/transform.md" + "normalizer/print-rules.md" "contributing.md" ]} diff --git a/scripts/update-markdown.sh b/scripts/update-markdown.sh index c7f5d3ce..05f5c97c 100755 --- a/scripts/update-markdown.sh +++ b/scripts/update-markdown.sh @@ -9,6 +9,7 @@ mdsh -i site/docs/src/quick-start.md --work_dir . mdsh -i site/docs/src/normalizer/dataize.md --work_dir . mdsh -i site/docs/src/normalizer/metrics.md --work_dir . mdsh -i site/docs/src/normalizer/transform.md --work_dir . +mdsh -i site/docs/src/normalizer/print-rules.md --work_dir . mdsh -i site/docs/src/contributing.md --work_dir . rm celsius.phi diff --git a/site/docs/src/SUMMARY.md b/site/docs/src/SUMMARY.md index b5b6f204..d8a8e216 100644 --- a/site/docs/src/SUMMARY.md +++ b/site/docs/src/SUMMARY.md @@ -14,4 +14,5 @@ - [normalizer pipeline prepare-tests](./normalizer/pipeline/prepare-tests.md) - [normalizer pipeline print-dataize-configs](./normalizer/pipeline/print-dataize-configs.md) - [normalizer pipeline report](./normalizer/pipeline/report.md) + - [normalizer print-rules](./normalizer/print-rules.md) - [Contributing](./contributing.md) diff --git a/site/docs/src/contributing.md b/site/docs/src/contributing.md index 956fdc10..076066ae 100644 --- a/site/docs/src/contributing.md +++ b/site/docs/src/contributing.md @@ -59,6 +59,7 @@ Available commands: metrics Collect metrics for a PHI program. dataize Dataize a PHI program. pipeline Run pipeline-related commands. + print-rules Print rules in LaTeX format. ``` Or, omit the executable name. @@ -80,6 +81,7 @@ Available commands: metrics Collect metrics for a PHI program. dataize Dataize a PHI program. pipeline Run pipeline-related commands. + print-rules Print rules in LaTeX format. ``` ## Docs diff --git a/site/docs/src/media/print-rules-tex-compact.png b/site/docs/src/media/print-rules-tex-compact.png new file mode 100644 index 00000000..bf691ddf Binary files /dev/null and b/site/docs/src/media/print-rules-tex-compact.png differ diff --git a/site/docs/src/media/print-rules-tex.png b/site/docs/src/media/print-rules-tex.png new file mode 100644 index 00000000..adbc1ea5 Binary files /dev/null and b/site/docs/src/media/print-rules-tex.png differ diff --git a/site/docs/src/normalizer.md b/site/docs/src/normalizer.md index e2e138ed..3f928f70 100644 --- a/site/docs/src/normalizer.md +++ b/site/docs/src/normalizer.md @@ -19,4 +19,5 @@ Available commands: metrics Collect metrics for a PHI program. dataize Dataize a PHI program. pipeline Run pipeline-related commands. + print-rules Print rules in LaTeX format. ``` diff --git a/site/docs/src/normalizer/dataize.md b/site/docs/src/normalizer/dataize.md index 46828675..30e6dc9d 100644 --- a/site/docs/src/normalizer/dataize.md +++ b/site/docs/src/normalizer/dataize.md @@ -91,7 +91,7 @@ Evaluating lambda 'Package' : ⟦ ⟧ Dataizing: Φ.org.eolang.float (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 40-39-00-00-00-00-00-00)) - Φ-dispatch: ⟦ + Phi: ⟦ c ↦ Φ.org.eolang.float (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 40-39-00-00-00-00-00-00)), result ↦ ξ.c.times (x ↦ ⟦ Δ ⤍ 3F-FC-CC-CC-CC-CC-CC-CD @@ -103,7 +103,7 @@ Evaluating lambda 'Package' : ⟦ λ ⤍ Package ⟧ . org.eolang.float (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 40-39-00-00-00-00-00-00)) - Φ-dispatch: ⟦ + Phi: ⟦ c ↦ Φ.org.eolang.float (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 40-39-00-00-00-00-00-00)), result ↦ ξ.c.times (x ↦ ⟦ Δ ⤍ 3F-FC-CC-CC-CC-CC-CC-CD @@ -239,7 +239,7 @@ Evaluating lambda 'Package' : ⟦ Δ ⤍ 40-40-00-00-00-00-00-00 ⟧ ) - ξ-dispatch: ⟦ + xi: ⟦ c ↦ Φ.org.eolang.float (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 40-39-00-00-00-00-00-00)), result ↦ ξ.c.times (x ↦ ⟦ Δ ⤍ 3F-FC-CC-CC-CC-CC-CC-CD @@ -257,14 +257,14 @@ Evaluating lambda 'Package' : ⟦ Δ ⤍ 40-40-00-00-00-00-00-00 ⟧ ) - R_DOT: Φ.org.eolang.float (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 40-39-00-00-00-00-00-00)).times (x ↦ ⟦ + DOT: Φ.org.eolang.float (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 40-39-00-00-00-00-00-00)).times (x ↦ ⟦ Δ ⤍ 3F-FC-CC-CC-CC-CC-CC-CD ⟧ ).plus (x ↦ ⟦ Δ ⤍ 40-40-00-00-00-00-00-00 ⟧ ) - Φ-dispatch: ⟦ + Phi: ⟦ c ↦ Φ.org.eolang.float (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 40-39-00-00-00-00-00-00)), result ↦ ξ.c.times (x ↦ ⟦ Δ ⤍ 3F-FC-CC-CC-CC-CC-CC-CD @@ -282,7 +282,7 @@ Evaluating lambda 'Package' : ⟦ Δ ⤍ 40-40-00-00-00-00-00-00 ⟧ ) - Φ-dispatch: ⟦ + Phi: ⟦ c ↦ Φ.org.eolang.float (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 40-39-00-00-00-00-00-00)), result ↦ ξ.c.times (x ↦ ⟦ Δ ⤍ 3F-FC-CC-CC-CC-CC-CC-CD diff --git a/site/docs/src/normalizer/print-rules.md b/site/docs/src/normalizer/print-rules.md new file mode 100644 index 00000000..2583f174 --- /dev/null +++ b/site/docs/src/normalizer/print-rules.md @@ -0,0 +1,126 @@ +# `normalizer print-rules` + +## CLI + +### `--help` + +```$ as console +normalizer print-rules --help +``` + +```console +Usage: normalizer print-rules [-r|--rules FILE] [--tex] [-c|--compact] + + Print rules in LaTeX format. + +Available options: + -r,--rules FILE FILE with user-defined rules. If unspecified, + yegor.yaml is rendered. + --tex Output LaTeX. + -c,--compact Print rules, each on a single line. + -h,--help Show this help text +``` + +### Default version + +```$ as tex +normalizer print-rules --tex +``` + +```tex +\begin{figure*} +\begin{tabular}{rl} + \rrule{Phi}: & $ Q $ \(\trans\) $ b $ \\\text {if }& $ Q -> b $ \\¬ in subformations\\\\ + \rrule{xi}: & $ \xi $ \(\trans\) $ b $ \\\text {if }& $ b $ is the scope of the redex\\¬ in subformations\\\\ + \rrule{DOT}: & $ [[ \tau -> b, B ]].\tau $ \(\trans\) $ \mathbb{S}(b, [[ \tau -> b, B ]]) $ \\\text {if }¬ in subformations,\\& $ b $ is nf inside formation,\\& $ [[ B ]]\in\mathcal{N} $ ,\\& $ \tau \neq ^ $ \\\\ + \rrule{DOTrho}: & $ [[ ^ -> b, B ]].^ $ \(\trans\) $ b $ \\\text {if }& $ [[ B ]]\in\mathcal{N} $ \\\\ + \rrule{phi}: & $ [[ B ]].\tau $ \(\trans\) $ [[ B ]].@.\tau $ \\\text {if }& $ @ \in B $ ,\\& $ \tau \notin B $ \\\\ + \rrule{COPY}: & $ [[ \tau -> ?, B1 ]]( \tau -> b1, B2 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B1 ]]( B2 ) $ \\\text {if }& $ b2 $ is the scope of the redex\\¬ in subformations,\\& $ b1\in\mathcal{N} $ \\\\ + \rrule{COPY1}: & $ [[ \tau -> ?, B ]]( 0-> b1 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B ]] $ \\\text {if }& $ b2 $ is the scope of the redex\\¬ in subformations,\\& $ b1\in\mathcal{N} $ \\\\ + \rrule{COPY2}: & $ [[ \tau1 -> ?, \tau2 -> ?, B ]]( 0-> b1, 1-> b2 ) $ \(\trans\) $ [[ \tau1 -> \mathbb{S}(b1, b3), \tau2 -> \mathbb{S}(b2, b3), B ]] $ \\\text {if }& $ b3 $ is the scope of the redex\\¬ in subformations,\\& $ b1\in\mathcal{N} $ ,\\& $ b2\in\mathcal{N} $ \\\\ + \rrule{COPYdelta}: & $ [[ D> ?, B ]]( D> y ) $ \(\trans\) $ [[ D> y, B ]] $ \\\text {if }¬ in subformations\\\\ + \rrule{EMPTY}: & $ [[ B1 ]]( ) $ \(\trans\) $ [[ B1 ]] $ \\\\ + \rrule{OVER}: & $ [[ \tau -> b1, B1 ]]( \tau -> b2, B2 ) $ \(\trans\) $ \dead $ \\\\ + \rrule{STOP}: & $ [[ B ]].\tau $ \(\trans\) $ \dead $ \\\text {if }& $ \tau, @, \lambda \notin B $ ,\\& $ ^ \in B $ ,\\& $ [[ B ]]\in\mathcal{N} $ \\\\ + \rrule{MISS}: & $ [[ B1 ]]( \tau -> b, B2 ) $ \(\trans\) $ \dead $ \\\text {if }& $ \tau, @, \lambda \notin B1 $ \\\\ + \rrule{DD}: & $ \dead.\tau $ \(\trans\) $ \dead $ \\\\ + \rrule{DC}: & $ \dead( B ) $ \(\trans\) $ \dead $ +\end{tabular} +\end{figure*} +``` + +The command above prints to the console rules from `yegor.yaml`, listing each condition of the rules on a separate line: + +![rules-latex](../media/print-rules-tex.png) + +```console +\begin{figure*} +\begin{tabular}{rl} + \rrule{Phi}: & $ Q $ \(\trans\) $ b $ \\\text {if }& $ Q -> b $ \\¬ in subformations\\\\ + \rrule{xi}: & $ \xi $ \(\trans\) $ b $ \\\text {if }& $ b $ is the scope of the redex\\¬ in subformations\\\\ + \rrule{DOT}: & $ [[ \tau -> b, B ]].\tau $ \(\trans\) $ \mathbb{S}(b, [[ \tau -> b, B ]]) $ \\\text {if }¬ in subformations,\\& $ b $ is nf inside formation,\\& $ [[ B ]]\in\mathcal{N} $ ,\\& $ \tau \neq ^ $ \\\\ + \rrule{DOTrho}: & $ [[ ^ -> b, B ]].^ $ \(\trans\) $ b $ \\\text {if }& $ [[ B ]]\in\mathcal{N} $ \\\\ + \rrule{phi}: & $ [[ B ]].\tau $ \(\trans\) $ [[ B ]].@.\tau $ \\\text {if }& $ @ \in B $ ,\\& $ \tau \notin B $ \\\\ + \rrule{COPY}: & $ [[ \tau -> ?, B1 ]]( \tau -> b1, B2 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B1 ]]( B2 ) $ \\\text {if }& $ b2 $ is the scope of the redex\\¬ in subformations,\\& $ b1\in\mathcal{N} $ \\\\ + \rrule{COPY1}: & $ [[ \tau -> ?, B ]]( 0-> b1 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B ]] $ \\\text {if }& $ b2 $ is the scope of the redex\\¬ in subformations,\\& $ b1\in\mathcal{N} $ \\\\ + \rrule{COPY2}: & $ [[ \tau1 -> ?, \tau2 -> ?, B ]]( 0-> b1, 1-> b2 ) $ \(\trans\) $ [[ \tau1 -> \mathbb{S}(b1, b3), \tau2 -> \mathbb{S}(b2, b3), B ]] $ \\\text {if }& $ b3 $ is the scope of the redex\\¬ in subformations,\\& $ b1\in\mathcal{N} $ ,\\& $ b2\in\mathcal{N} $ \\\\ + \rrule{COPYdelta}: & $ [[ D> ?, B ]]( D> y ) $ \(\trans\) $ [[ D> y, B ]] $ \\\text {if }¬ in subformations\\\\ + \rrule{EMPTY}: & $ [[ B1 ]]( ) $ \(\trans\) $ [[ B1 ]] $ \\\\ + \rrule{OVER}: & $ [[ \tau -> b1, B1 ]]( \tau -> b2, B2 ) $ \(\trans\) $ \dead $ \\\\ + \rrule{STOP}: & $ [[ B ]].\tau $ \(\trans\) $ \dead $ \\\text {if }& $ \tau, @, \lambda \notin B $ ,\\& $ ^ \in B $ ,\\& $ [[ B ]]\in\mathcal{N} $ \\\\ + \rrule{MISS}: & $ [[ B1 ]]( \tau -> b, B2 ) $ \(\trans\) $ \dead $ \\\text {if }& $ \tau, @, \lambda \notin B1 $ \\\\ + \rrule{DD}: & $ \dead.\tau $ \(\trans\) $ \dead $ \\\\ + \rrule{DC}: & $ \dead( B ) $ \(\trans\) $ \dead $ +\end{tabular} +\end{figure*} +``` + +### Compact version + +The compact version prints rules listing all conditions on a single line: + +```$ as tex +normalizer print-rules --tex --compact +``` + +```tex +\begin{figure*} + \rrule{Phi}: $ Q $ \(\trans\) $ b $ \quad\text {if } $ Q -> b $ , not in subformations\\\vspace*{0.5em} + \rrule{xi}: $ \xi $ \(\trans\) $ b $ \quad\text {if } $ b $ is the scope of the redex, not in subformations\\\vspace*{0.5em} + \rrule{DOT}: $ [[ \tau -> b, B ]].\tau $ \(\trans\) $ \mathbb{S}(b, [[ \tau -> b, B ]]) $ \quad\text {if }not in subformations, $ b $ is nf inside formation, $ [[ B ]]\in\mathcal{N} $ , $ \tau \neq ^ $ \\\vspace*{0.5em} + \rrule{DOTrho}: $ [[ ^ -> b, B ]].^ $ \(\trans\) $ b $ \quad\text {if } $ [[ B ]]\in\mathcal{N} $ \\\vspace*{0.5em} + \rrule{phi}: $ [[ B ]].\tau $ \(\trans\) $ [[ B ]].@.\tau $ \quad\text {if } $ @ \in B $ , $ \tau \notin B $ \\\vspace*{0.5em} + \rrule{COPY}: $ [[ \tau -> ?, B1 ]]( \tau -> b1, B2 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B1 ]]( B2 ) $ \quad\text {if } $ b2 $ is the scope of the redex, not in subformations, $ b1\in\mathcal{N} $ \\\vspace*{0.5em} + \rrule{COPY1}: $ [[ \tau -> ?, B ]]( 0-> b1 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B ]] $ \quad\text {if } $ b2 $ is the scope of the redex, not in subformations, $ b1\in\mathcal{N} $ \\\vspace*{0.5em} + \rrule{COPY2}: $ [[ \tau1 -> ?, \tau2 -> ?, B ]]( 0-> b1, 1-> b2 ) $ \(\trans\) $ [[ \tau1 -> \mathbb{S}(b1, b3), \tau2 -> \mathbb{S}(b2, b3), B ]] $ \quad\text {if } $ b3 $ is the scope of the redex, not in subformations, $ b1\in\mathcal{N} $ , $ b2\in\mathcal{N} $ \\\vspace*{0.5em} + \rrule{COPYdelta}: $ [[ D> ?, B ]]( D> y ) $ \(\trans\) $ [[ D> y, B ]] $ \quad\text {if }not in subformations\\\vspace*{0.5em} + \rrule{EMPTY}: $ [[ B1 ]]( ) $ \(\trans\) $ [[ B1 ]] $ \\\vspace*{0.5em} + \rrule{OVER}: $ [[ \tau -> b1, B1 ]]( \tau -> b2, B2 ) $ \(\trans\) $ \dead $ \\\vspace*{0.5em} + \rrule{STOP}: $ [[ B ]].\tau $ \(\trans\) $ \dead $ \quad\text {if } $ \tau, @, \lambda \notin B $ , $ ^ \in B $ , $ [[ B ]]\in\mathcal{N} $ \\\vspace*{0.5em} + \rrule{MISS}: $ [[ B1 ]]( \tau -> b, B2 ) $ \(\trans\) $ \dead $ \quad\text {if } $ \tau, @, \lambda \notin B1 $ \\\vspace*{0.5em} + \rrule{DD}: $ \dead.\tau $ \(\trans\) $ \dead $ \\\vspace*{0.5em} + \rrule{DC}: $ \dead( B ) $ \(\trans\) $ \dead $ +\end{figure*} +``` + +![rules-latex-compact](../media/print-rules-tex-compact.png) + +```console +\begin{figure*} + \rrule{Phi}: $ Q $ \(\trans\) $ b $ \quad\text {if } $ Q -> b $ , not in subformations\\\vspace*{0.5em} + \rrule{xi}: $ \xi $ \(\trans\) $ b $ \quad\text {if } $ b $ is the scope of the redex, not in subformations\\\vspace*{0.5em} + \rrule{DOT}: $ [[ \tau -> b, B ]].\tau $ \(\trans\) $ \mathbb{S}(b, [[ \tau -> b, B ]]) $ \quad\text {if }not in subformations, $ b $ is nf inside formation, $ [[ B ]]\in\mathcal{N} $ , $ \tau \neq ^ $ \\\vspace*{0.5em} + \rrule{DOTrho}: $ [[ ^ -> b, B ]].^ $ \(\trans\) $ b $ \quad\text {if } $ [[ B ]]\in\mathcal{N} $ \\\vspace*{0.5em} + \rrule{phi}: $ [[ B ]].\tau $ \(\trans\) $ [[ B ]].@.\tau $ \quad\text {if } $ @ \in B $ , $ \tau \notin B $ \\\vspace*{0.5em} + \rrule{COPY}: $ [[ \tau -> ?, B1 ]]( \tau -> b1, B2 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B1 ]]( B2 ) $ \quad\text {if } $ b2 $ is the scope of the redex, not in subformations, $ b1\in\mathcal{N} $ \\\vspace*{0.5em} + \rrule{COPY1}: $ [[ \tau -> ?, B ]]( 0-> b1 ) $ \(\trans\) $ [[ \tau -> \mathbb{S}(b1, b2), B ]] $ \quad\text {if } $ b2 $ is the scope of the redex, not in subformations, $ b1\in\mathcal{N} $ \\\vspace*{0.5em} + \rrule{COPY2}: $ [[ \tau1 -> ?, \tau2 -> ?, B ]]( 0-> b1, 1-> b2 ) $ \(\trans\) $ [[ \tau1 -> \mathbb{S}(b1, b3), \tau2 -> \mathbb{S}(b2, b3), B ]] $ \quad\text {if } $ b3 $ is the scope of the redex, not in subformations, $ b1\in\mathcal{N} $ , $ b2\in\mathcal{N} $ \\\vspace*{0.5em} + \rrule{COPYdelta}: $ [[ D> ?, B ]]( D> y ) $ \(\trans\) $ [[ D> y, B ]] $ \quad\text {if }not in subformations\\\vspace*{0.5em} + \rrule{EMPTY}: $ [[ B1 ]]( ) $ \(\trans\) $ [[ B1 ]] $ \\\vspace*{0.5em} + \rrule{OVER}: $ [[ \tau -> b1, B1 ]]( \tau -> b2, B2 ) $ \(\trans\) $ \dead $ \\\vspace*{0.5em} + \rrule{STOP}: $ [[ B ]].\tau $ \(\trans\) $ \dead $ \quad\text {if } $ \tau, @, \lambda \notin B $ , $ [[ B ]]\in\mathcal{N} $ \\\vspace*{0.5em} + \rrule{MISS}: $ [[ B1 ]]( \tau -> b, B2 ) $ \(\trans\) $ \dead $ \quad\text {if } $ \tau, @, \lambda \notin B1 $ \\\vspace*{0.5em} + \rrule{DD}: $ \dead.\tau $ \(\trans\) $ \dead $ \\\vspace*{0.5em} + \rrule{DC}: $ \dead( B ) $ \(\trans\) $ \dead $ +\end{figure*} +``` diff --git a/site/docs/src/pipeline.md b/site/docs/src/pipeline.md index 4bccfc1a..88ac46da 100644 --- a/site/docs/src/pipeline.md +++ b/site/docs/src/pipeline.md @@ -31,7 +31,7 @@ node --version ``` ```console -v20.16.0 +v20.17.0 ``` Install [Java](https://www.java.com/en/download/help/download_options.html).