abella

abella copied to clipboard

The reasoning level of Abella has an extend-only pseudo module system. It could benefit from a real module system with support for proper lemmas and instantiating declared lemmas and constants...

chaudhuri

Support bytecode-only target for 32-bit platforms like powerpc

29

While 2.0.7 built fine (after fixing bytecode target), 2.0.8 fails now: ``` ---> Building abella Executing: cd "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-2.0.8" && /usr/bin/make -j6 -w all make: Entering directory `/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-2.0.8' dune build src/abella.exe...

barracuda156

Build fails: Error (warning 70 [missing-mli]): Cannot find interface file.

7

Build fails on some systems: ``` ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/extensions.cmo src/extensions.ml + ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src...

yurivict

This is based on [this thread](https://groups.google.com/d/msgid/abella-theorem-prover/e69e80af-313f-4610-9d30-5401f99d480fn%40googlegroups.com?utm_medium=email&utm_source=footer) on the mailing list started by Todd Wilson (@lambdacalculator). His example: ``` Kind t type. % Close t. Theorem member_prune[A] : forall E (L:list...

chaudhuri

Running Abella in the browser

2

Inspired by @jcreedcmu's recent success with getting Twelf to run in the browser (see https://github.com/jcreedcmu/twelf-wasm), I wanted to see if we could get something similar working for Abella. TL;DR: I...

tausbn

Variable confusion/ill typed terms with higher-order terms

4

Script: ``` Kind expr type. Type mu ((expr -> expr) -> expr) -> expr. Define foo : expr -> expr -> prop by foo (mu k\ E k) (mu k_\...

wikku