Ryan's Tutorial Feedback

[rtzam]

Before the basics

The big question I have is "who's the audience". I recommend literally write down who your target audience is in an intro section so folks know what their getting into.
A decent reference might be the LLVM Frontend Tutorial

Getting setup

I recommend the tutorial have a "Getting Setup" landing page.
This shouldn't be a duplicate of the installation instructions found on the Github, but a pointer to those plus communicate a rough idea of how to run code. For example "Let get setup! here's the link to the installation instructions you should follow... make sure to have the binary available on your command line". Then some other specifics worth addressing:

• What version does the tutorial expect users to have installed?
  • built from main or a particular release?
• How should we write and run files?
  • written using the .egg extension or a .scm?
  • run via the web demo, cargo run, or an installed egglog? Perhaps with specific flags --no-messages?

[rtzam]

Basics 01

I'm concerned that centering this egglog tutorial around associative and commutative operators and rewrites is a big risk. It seems like users could accidently hit the "hockey stick" part of egglog performance and feel disenfranchised, confused etc. I think choosing a domain where operators and rewrites are more well-behaved is a safer choice for a tutorial. Another option is to let the users know that we are treading in murky waters w.r.t AC ops.

Mental Model of an Egglog program

Throughout this section, certain terms are used in a way that reflects a particular mental model of egglog and the egraph. Although it may feel natural to some, there are casual context swaps between egglog and the underlying egraph that are jarring for others. For example, when writing the expr1 and expr2 we refer to these as "expressions". However, later on when discussing what rules match on, we refer to "egraph terms". However, the difference between egglog and the underlying egraph has not been established. The casual violations of the absraction boundaries between the two leads to confusion. Where does the language end and the egraph begin?

The challenge here is to delicately begin developing a mental model of the semantics of the language.
For example, "when I type this expression, it does this to the egraph".

Here's another specific example of this:

Rules are not instantiated for every possible term; they are only instantiated for terms that are in the e-graph.

However, is hasn't been discussed what's in the egraph and when it's added.

Side notes:

• Does egglog manage one egraph or multiple?
• What's an expression vs. a term? Is one for language level vs egraph level things?
• When we write an expression are we introducing terms into the egraph?
• There's an implicit state threaded through and modified by each egglog statement and the

Specifics

• I think the info that egglog logs to the terminal is worthy of explanation (or suppression). The logs get ahead of the tutorial by displaying extraction cost. Given that you include expected print output and that the log deviates from that, I feel this must be addressed.
• when I run (check (= expr1 (Mul x y))) there is a lot of stuff printed that obscures whether that checked passed. In the writing it is unclear if this check should succeed at this point. Please say that passing returns an "INFO" object
• instead of "where x and y are variables that can be mapped to any expression in the e-graph." talk about that they are patterns or wildcards or something that egglog can pattern match to. As of now, the use of "variable" is too overloaded (an Expr variable, and egglog variable like expr1, a pattern variable). In fact, the syntax to use an egglog variable or a pattern variable are identical so it's not clear from context what x and y are. It feel like an error. We also use (Var "x") in our assignment of expr1 so it could even read like a typo in the tutorial (I thought this at first).
• have the user run the failing ; (check (= expr1 (Add x y))) so that they see what an error looks like
• You have not discussed how to "run" rules at this time of this quote:

For instance, even if we run the commutativity rule above, the following check would still fail

• If visualizing the egraph is important, should everyone be using the web demo for the tutorial? Is it more important to teach folks how to use the binary to generate this same visualization. If so, then this should be described precisely

If you are running the program in the web demo, in the bottom right corner, you should see an e-graph with two expressions, each corresponding to the two expressions we defined above.

and

If you are using the web demo, after running the rules, you should see the e-graph has grown a little bit

• Add something either say what the output should be or tell the user to run this example

(extract (+ "1" "2"))
(extract (+ 1.0 2.0))

In the final check

(check (= expr1 expr2))

There is logged output about the number of matches. This is important information. Should it be talked about?

Nits

• a code markup is egglog when referring to the language in abstract. Code markup should be reserved for literal code (i.e. when invoking the egglog binary from the terminal) and egglog should be refered to as a proper noun. The other usages are code markup are for egglog syntax.
• the phrase "constant folding" is compiler-optimization specific jargon. I recommend trying another phrase not compiler specific

The following rules show constant folding over addition and multiplication.

[rtzam]

Datalog 02

In the last lesson, we write our first equality saturation program in egglog

No, we didn't. We never used (saturate), we only (run 10)

One of the benifits of egglog being a language for program optimization is that it can talk about terms natively, so in egglog we get Datalog with terms for free.

I don't understand this sentence. It feels like a non-sequitur: why does egglog being for program optimization mean we get terms for free?

In this lesson, we will define multiple relations with the same name, so we use the (push) and (pop) commands to clone and reset the database

What database? This sentence completely shifts both the audience and the abstraction provided by egglog here. Should the reader of the whole tutorial be familiar with egglog, set theory, e-graphs, or something else? Should the reader skip certain sections if they are missing some background? Are certain sections for certain folks? Secondly, is egglog an abstraction of an egraph, a database, or both? How should the tutorial reader expand/change their mental model established in tutorial one based on this new database stuff?

This database vs. egraph switch is pervasive throughout this lesson.
By putting this tutorial out for the world, you are establishing some amount of egglog pedagogy. It is normative document of how newcomers should think about egglog.
Is is totally acceptable to have multiple mental models simultaneously (sometimes a database and sometimes an egraph). However, it must be made really obvious that these are two sides of the same coin!

A rule has the form (rule (atom1 atom2 ..) (action1 action2 ..))

Why are they called atom when they can be general patterns?

For the rule we have just defined, the only atom is (path a b), which asks egglog to search for possible a and bs such that (path a b) is a fact in the database.

Is this correct? shouldn't this be all (edge a b) instead? It also remains to be said that for all a and b that match fit the pattern, a new member is added to the path relation.

Again, defining a rule does not mean running it in egglog

Should read "defining a rule does not immediately run it in egglog"

Exercises

This section header appears twice. The first one feels like a mistake because most of the content is new information.

A relation is just a function with output domain Unit.

and

We have talked about relations being a special case of functions

Isn't the opposite true, mathematically (i.e. that all functions are relations but not all relations are functions)? However, if I am correct here, you're discussing some egglog-specific design choice that feels backwards. Is this true in datalog as well? Can you add a clarification that you're not talking about the math here, but an egglog quirk. Why was this design adopted?

But we can also assert that edge does not have a merge expression using no-merge.

Should read that "we must assert" that the edge does not have a merge. Egglog throws an error otherwise.

If a conflict happens, egglog will panic.

instead of panic which is a very Rust specific thing, perhaps "report an error"?

This block of code should be broken up into two separate sections

(run-schedule (saturate (run)))
(check (= (path 1 3) 20))

(pop)
(push)

Now let us combine the knowledge we have learned in lessons 1 and 2 to write a program that combines both equality saturation and Datalog.

should read "lessons 1 and this lesson so far".

For instance, (rewrite (Add a b) (Add b a)) is lowered to the following rule: (rule ((= e (Add x y))) ((union e (Add y x))))

The rule statement has not been introduced yet. I know it's about to be. Just wait a little longer!