Mnemo

(Apollo dancing with the Muses)
Mnemosyne provides automated software development collaborators or "muses."

Mnemosyne

Mnemosyne: Titan goddess of memory and remembrance, inventor of language, mother of the muses.

Read about Mnemosyne's relationship to GitHub's CoPilot.

Mnemosyne is your automated software development assistant. It integrates with your IDE and works with you suggesting code, types, and tests as you work; and continually checking the consistency of your documentation, types, tests, and implementation—whether that means running test suites or type checkers, or using ML techniques to ensure your documentation matches your implementation. Mnemosyne applies statistical machine learning, formal methods, and Search Based Software Engineering (SBSE) to enable developers to write higher quality, higher assurance, and more standards compliant code more quickly. Mnemosyne transcends CI/CD by making live substantive contributions to the software development process as the developer works. Mnemosyne speaks LSP, meaning it integrates seamlessly with most popular text editors and IDEs. Mnemosyne is extensible, easily collaborating with varied program synthesis modules or "Muses."

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.

Argot

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.

Mnemosyne Architecture

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:

NameDescriptionVideo
Argument Predictor probabilistic completion of callsite arguments
DIG trace-based invariant generation technique
Galois Autocomplete machine learning based code completion
GenPatcher automated program repair
Herbie improve floating-point code stability and accuracy
Hypothesis Tests type-driven automated testing
Snippet Mining example API usage snippets
SSR AST-level software search and replace
Trinity extensible systhesis framework for data science

Note: Due to an open bug in GitLab's pages feature (gitlab-pages#504, forum/44691) videos don't render in Safari.

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.

Copyright (C) 2021 GrammaTech, Inc.

This material is based upon work supported by the US Air Force, AFRL/RIKE and DARPA under Contract No. FA8750-20-C-0208. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the US Air Force, AFRL/RIKE or DARPA.