Mnemosyne

QuickStart

See Usage for detailed usage information.

1. Install docker-compose.

2. Clone the Argot Server repository.

   git clone https://gitlab.com/GrammaTech/Mnemosyne/argot-server.git

3. In the argot-server directory, start Argot Server.

   make up

   If you need to run on the host network (e.g. you are using a restrictive VPN), use host-up instead.

   make host-up

   If you have a GPU, and Docker is configured to work with it, you can pass GPU=1:

   GPU=1 make up

4. Open a C, C++, Python, JavaScript, or Common Lisp file and connect your editor or IDE to the server.

   From Visual Studio Code:

   1. Install the latest Mnemosyne VS Code extension. (How to install a .vsix file.)
   2. Open Command Palette (Control+Shift+P) and connect to the Argot Server with Mnemosyne: Connect to Argot Server.
   3. Click on the code action “bulb” icon or request code actions with Control+.

   From Emacs:

   1. Install Eglot M-x package-install-package eglot RET.
   2. Add eglot-argot.el to your load path and (require ‘eglot-argot).
   3. Connect to the Argot Server with M-x eglot using localhost:10003 for the host and port.
   4. Invoke Mnemosyne with M-x eglot-code-actions.

   From Vim:

   1. Install coc.nvim and coc-argot with Plug:

      Plug 'neoclide/coc.nvim', {'branch': 'release'}
      Plug 'https://gitlab.com/GrammaTech/Mnemosyne/coc-argot',
      \ {'do': 'npm install && npm run compile'}
      

   2. Connect to the Argot Server with CocCommand mnemosyne.connect.
   3. Use :CocAction to request Mnemosyne code actions.

Architecture

See System Architecture for detailed design information.

Mnemosyne extends Microsoft's LSP protocol for IDE integration to support decorating program subtrees with tests, types, and prose. We call this extension "Argot LSP," or “Argot” for short.

Inside Mnemosyne Argot allows automated techniques of program test generation, program analysis, type and invariant inference, and program synthesis and refactoring (we call these modules "Muses") to communicate with each other as well as with the developer's IDE.

The result is a collaborative environment centered around the developer where suggestions for new tests, types, and code edits are continually made against the software code base. The result is improved developer productivity and software quality.

Muses

See Muses for a complete list of the Modules or Muses currently implemented and under development for Mnemosyne with demo videos. Some of these include:

See multi-muse flows for examples of multiple Muses collaborating to automate larger scale development tasks.

Goals and Approach

See About for general information about the project and Approach for our top-level themes and approaches to human/computer collaboration.

The Mnemosyne project was started by GrammaTech in collaboration with leading program synthesis researchers: Swarat Chaudhuri and Işıl Dillig from UT Austin, and Armando Solar-Lezama from MIT.

Research in program synthesis and automated software engineering has leapt forward in recent years thanks to advances in underlying machine learning and constraint solving technologies. We hope to bridge research and practice by connecting research technologies to modern programming languages and IDEs. To ensure practical utility we focus on the following themes:

• Transparency: All results of muses are displayed to the developer using familiar tests, types, and code edits.
• Interactivity: The developer's activities guide muses and curate their results. Smaller more focused developer interactions are prioritized over coarse-grained large-scale synthesis.
• Incrementality: Intermediate results are communicated back to the developer and the software project. Synthesis techniques that proceed function by function are prioritized when scalability is in question.