CS 4ZP6A CAPSTONE
Content
- Project Goal
- Group Members
- Demo
- Technology Stack
- Versions
- Language Considerations
- Available Test Cases
- How To Add Test Cases
- CI Workflow - Run System
- CLI
- Graph Generation
- Website
- Sources
Group Members
- Proyetei Akanda
- Esha Pisharody
- Zainab Abdulsada
- Grace Croome
- Marie Hollington
- Emma Willson
Project Goal
The goal of this capstone project is to design and build an automated code generator that creates a series of tests of increasing size that will test the efficiency of modern interactive proof assistants including Lean, Idris, Agda, and Rocq. Testing will be performed on these assistants as languages, outside of their specific capabilities as proof assistants. The project will also include a command line interface enabling users to view the time and memory complexity and provide a link redirecting them to local webpages presenting visualizations of the measured data.
Demo
This is an example output for test case 9 - NewLineFile with an upper bound of 100,000 and 50 data points, view it here -> https://capstone-proyeteis-projects.vercel.app/
Please run GitHub Actions to run your own tests! (Click on "Actions" and view the CI Workflows Section)
Technology Stack
- Haskell for building the translators, grammars, and the automated code generator creating test cases for each of the 4 proof assistants (Idris, Agda, Lean, Rocq)
- Includes a CI/CD pipeline in GitHub Actions to run the tests using Go + Docker and generating JSON file with the benchmarking results
- Flask + Python for the backend
- HTML/Tailwind CSS/JavaScript for frontend
- Vercel for deployment
Versions
- Python (3.12.3)
- Flask (3.10.1)
- Lean (4.17.0)
- Idris2 (0.7.0)
- Rocq (8.20.1)
- Agda (2.7.0.1)
- Nix Channel (24.11 and Unstable)
- Docker (26.1.3)
- GHC (9.4.7)
- Cabal (3.8.1.0)
- Go (1.23.6)
Log in or sign up for Devpost to join the conversation.