andrejbauer / alg Goto Github PK

There appears to be a manual included but only as a Tex file. It could be nice if it was provided in a way that could be more readable as is. Thanks.

It seems that eventual_period in unary_invariant and binary_invariant is needlessly quadratic time. If we keep track of when we saw each element, then when an element re-appears, we will instantly know that we already saw it. So the complexity ought to be linear.

For the following file:

Axiom: (forall x, True).

I get the error:

Syntax error at line 0, characters 8-14:
I got confused here

In particular, alg can't parse theories/group_inefficient.th.

Figure out which commit was the last one before I started mocking about and branch it off into stable.

The Makefile depends on ocamlbuild, but instructions only install ocaml and menhir.

The saving/loading appears not to speed the computation at all. Perhaps it does not work?

A la http://plzoo.andrej.com/

It looks like alg used menhir from the very start. I suggest we keep using it. We'll provide binaries for people on Windows anyway.

Change installation procedure so it uses autoconf.

Why do we have eval functions in eval.ml as well as in first_order.ml?

Binaries are currently not available on the website http://math.andrej.com/alg/.

Can I suggest that you use GitHub releases to host them? I found this very convenient for my projects.

P.S.: Thank you for the great tool!

Abstract sytnax does not keep the source code locations. This is bad because error reporting cannot give information about where an error occurred.