Move non-DDM commands out of StrataMain

[tautschnig]

See #405 (comment): lake exe strata ... will now do both DDM commands as well as uses of Strata as a program analysis tool. We should aim for a user experience that has the least amount of surprise and should, therefore, move the non-DDM commands to a separate CLI.

[joehendrix]

Thanks, I'm thinking of keeping them but using groups. strata --help would produce something like the text below.

Do you think that would address the concern?

Usage: strata <command> [flags]...                                                                                                           
                                                                                                                                             
  Command-line utilities for working with Strata dialect and program files.                                                                    
                                                                           
  Core:                                                                                                                                        
    check <file>                                                           
        Parse and validate a Strata file (text or Ion). Reports errors and exits.

    toIon <input> <output>
        Convert a Strata text file to Ion binary format.

    print <file>
        Pretty-print a Strata file (text or Ion) to stdout.

    diff <file1> <file2>
        Compare two program files for syntactic equality. Reports the first
        difference found.

    Common flags:
      --include <path>  Add a dialect search path.

  Python:
    pyAnalyze <file>
        Verify a Python Ion program. Translates Python to Core, inlines
        procedures, and runs SMT verification.
      Flags:
        --verbose  Enable verbose output.

    pyAnalyzeLaurel <file>
        Verify a Python Ion program via the Laurel pipeline. Translates Python
        to Laurel to Core, then runs SMT verification.
      Flags:
        --verbose  Enable verbose output.

    pyTranslate <file>
        Translate a Python Ion program to Core and print the result to stdout.

    pySpecs <python_path> <strata_path>
        Translate a Python specification (.py) file into Strata DDM Ion format.
        Creates the output directory if needed. (Experimental)

    pySpecToLaurel <python_path> <strata_path>
        Translate PySpec DDM declarations from an existing Ion file into Laurel
        and print a summary.

  Laurel:
    laurelAnalyze
        Read Laurel Ion programs from stdin, verify, and print diagnostics.
        Multiple files are combined before verification.

  Java:
    javaGen <dialect-file> <package> <output-dir>
        Generate Java source files from a DDM dialect definition. Writes .java
        files under output-dir.
      Flags:
        --include <path>  Add a dialect search path.

[tautschnig]

I think groups is a great idea, but I'd still like to see a bit more separation by use case - perhaps that just means different group names? On a cursory look it would seem that both "Python" and "Java" groups are for similar use cases, just different input languages. The actual subcommands, however, are entirely different: javaGen produces files so as to use Strata from a Java program, while all of the py* subcommands seem related to analysis of Python code.

[joehendrix]

Yes, I debated whether to put the command in a separate Java group or just put it in Core. I decided Java was as good as name as any.

Do you have a concrete new group scheme? I just want the extra flag functionality of #451 for another use case - I do not care at all what the category names are.

[keyboardDrummer]

I would prefer using subcommands instead of groups, so you don't have to repeat part of the group name in the command name for it to be unique. Commands with similar options should have the same parent command, so the "biggest choices" end up as top commands. My suggestion would be:

• verify (verify source code)
  • python. (replaces pyAnalyze, pyAnalyzeLaurel and pyTranslate)
    Has options --backend=Laurel(default)|Core, --print-Core=<out> and --halt-after-print
  • laurel (replaces laurelAnalyze)
  • ...input languages
• prepare (prepare the verification of a library)
  • python (replaces pySpecs and pySpecsToLaurel)
• integrate (integrate with a system written in a non-Lean language)
  • java (replaces javaGen)
  • ..other languages that we want to support integration with

verify would have as options, among many others, --input=Source|Ion, various --print-<language>=<out> options, --halt-after-print.

[aqjune-aws]

Hi, is this issue resolved?