Update TODO.

eval: Split running external code according to return type.

Previously we were wrongly hiding stdout in some cases.

Fixes commit a48b05d35f0646322e8178ff10f8ed7af3e739aa
and commit 2ac1b84cb49ad04e27b4543436b0227153fbfb15.

Implement pure functions.

lexer: Use @{...} for quiet code sections.

parser: Fix parsing of patterns containing explicit tactic names.

parser: Fix tracking of beginning of line for error messages.

Copy system environment into initial env, and also add %stdlib.

Allow functions "returning strings" (etc), redefine sort function.

Standardize running code in a single function, include prelude.sh.

Update TODO

Functions return expressions instead of only lists of strings.

build: Create dependencies for Goalfile itself.

stdlib: Implement sort function.

Update TODO.

build: Generate complete OCaml dependencies.

Because we didn't use -I src on the ocamldep command line, ocamldep
didn't generate the complete set of dependencies.

Ast: Standard location for ocamldoc comments.

stdlib: Implement wildcard function.

Implement functions.

Ast: Remove functions which were moved to Eval module.

Updates commit f36210fd16a8e4e4d6ecdd8825bf8b8307943472.

build: Add depend goal and 'make depend'.

build: Don't always pass -d to goals.

We can enable debugging on a case-by-case basis when necessary.

build: Fix construction of parser.mli

build: Fix ocamldep invocation.

build: Fix 'goals clean' rule.

stdlib: Fix *file tactic.

Broken test if there is more than one dependency.

run: Fix whitespace.

run: Better debugging and error messages for goals and tactics.

run: If multiple goals match a tactic, at most one must have a CODE section.

This now works the same way as make.

Don't default to echoing tactic command.

Update TODO

In dependency file, use ; between statements.

So this parses correctly.

parser: Optional semicolon between statements.

Simplify Constructor -> Ctor.

Rename Eval -> Run, split out some Ast functions into new Eval.

This gives us more consistent nomenclature:

  - "Run" for running targets.
  - "Eval" for simplifying and evaluating expressions, etc.
  - "Ast" is a library of AST-related structures.

eval: Don't check target was rebuilt if there is no code.

A pure dependency rule like:

  "foo.o": "foo.c"

doesn't contain any code, so it doesn't make sense to check if the
target has been rebuilt.

Use goals itself exclusively to build.

eval: Goals with no targets always need a rebuild.

eval: If multiple goals match a tactic, run them all.

lexer: Fix parsing of { characters in CODE sections.

eval: Explicit function to evaluate goal arguments.

Revert "eval: Expand goal args before running the goal."

This reverts commit 8509cad9b10205b7bec23eb59ba63e88c3d0fcb3.

eval: Expand goal args before running the goal.

Lexer: Allow "-" char in the middle of identifier names.

This allows eg maintainer-clean to be a goal name.

Ast: Rename ECallTactic to ETacticConstructor.

This is a constructor, it's not 'calling' anything.

Ast: Change EGoal -> EGoalDefn, ETactic -> ETacticDefn.

Implement -include (optional include) command.

Fix ‘goal’ when it appears as a target (meaning ‘goal()’).

More TODO ideas.

Add some more debugging.

Implement -d (debug) option.

Change -V to -v for compat with make.

stdlib: Add some rules for OCaml code.

Implement stdlib directory, -I, --no-prelude, etc.

Define OCaml Config module in ./configure, ./run script, --version option.

Implement tactics.

Remove Ast.PVar.

Pure variables as patterns are disallowed.  Patterns have a distinct
type from expressions so allowing an expression to be substituted
causes complications.  In particular we want to know statically how
many targets a goal has, which is not possible if a variable can be
substituted here.

You can still write:

  "%name": ...

Run code with set -e / set -x.

Actually run goal code.

Add implicit tactic rebuild.

We don't need to look for a goal covering every tactic, if the tactic
doesn't need rebuilding.

Substitute %<, %@ etc variables into code.

Add Ast.to_shell_script.

Previously we were confusing Ast.substitute with the place where we
need to shell quote.

Hard code *file tactic.

Implement tactic matching.

todo: Note default parameters.

Factor out param_decl and improvements to AST printing.

Refactor evaluation.

Also more work on pattern matching and when to rebuild.

Fix file() -> *file() in comment about tactics.

Updates commit b14ff66c953e6a73e9ac2fe8d42dd68e92e58f53.

Rename Ast.StringMap -> Ast.Env

Begin converting Ast print functions so they can be used with format %a.

Send debug message to stderr.

Print errors (Failure exceptions) nicely.

Define *file() syntax for tactic constructors.

Alternative syntaxes considered where ~file and &file.

Attach parser location information to AST nodes.

Basic evaluation.

Implement -C / --directory option.

Add environment to store variables and goals.

Command line parsing of anon args.

Expose parsing of expressions from command line.

Continue command line parsing.

Rename parsing/ to src/

And some refactoring of the main code and command line parsing.

Initial commit of parser.