debugging meta.yml

meta.yml

---
# configuration file for [coq-community templates](https://github.com/coq-community/templates)
fullname: cpp2v
shortname: cpp2v
organization: bedrocksystems
community: false
travis: false

synopsis: >-
  Axiomatic semantics for C++ built on top of Clang and Iris including
  a tool to convert C++ files into Coq ASTs
description: |-
  This project provides an axiomatic semantics for C++ programs built on
  top of the Iris framework for separation logic.
  The AST is based on the AST of Clang and the project contains a standalone
  tool and Clang plugin that convert C++ files into their AST.

# publications:

authors:
- name: Gregory Malecha
  initial: true
- name: Gordon Stewart
  initial: false
- name: Abhishek Anand
  initial: false
- name: John Grosen
  initial: false

maintainers:
- name: Gregory Malecha
  nickname: gmalecha

dependencies:
- opam:
    name: coq-ext-lib
    version: '{(>= "0.11.1")}'
- opam:
    name: coq-iris
    version: '{(= "dev.2020-03-16.0.62be0a86")}'
- opam:
    name: conf-clang

opam-file-maintainer: [email protected]

opam-file-version: dev

license:
  fullname: GNU Affero General Public License
  identifier: AGPL-3.0

supported_coq_versions:
  text: master (use the corresponding branch or release for other Coq versions)
  opam: '{>= "8.11.0" && < "8.12~"}'

supported_ocaml_versions:
  text: 4.05.0 or later
  opam: '{>= "4.05.0"}'

# tested_coq_nix_versions:
# - version_or_url: https://github.com/coq/coq-on-cachix/tarball/master

tested_coq_opam_versions:
- version: dev

namespace: bedrock

keywords:
- name: c++
- name: axiomatic semantics
- name: separation logic
- name: program verification

# categories:
# - name: Miscellaneous/Coq Extensions
# - name: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures

documentation: |
  # cpp2v

  Tool for converting C++ files into Coq files.

  ## Running

  ### As a standalone tool

  ```sh
  cpp2v -v -names XXX_names.v -o XXX_cpp.v XXX.cpp -- ...clang options...
  ```

  ### As a plugin

  ```sh
  clang -Xclang -load -Xclang ./libcpp2v_plugin.so -Xclang -plugin -Xclang cpp2v -Xclang -plugin-arg-cpp2v -Xclang -o -Xclang -plugin-arg-cpp2v -Xclang foo_cpp.v
  -Xclang -plugin-arg-cpp2v -Xclang -names -Xclang -plugin-arg-cpp2v -Xclang foo_names_cpp.v ...standard clang options...
  ```

  ## Build & Dependencies

  ### Linux (Ubuntu)

  The following script should work, but you can customize it based on what you have:

  ```sh
  sudo apt install llvm-9 llvm-9-dev clang-9 libclang-9-dev cmake opam
  # install opam dependencies
  opam repo add coq-released https://coq.inria.fr/opam/released
  opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
  opam pin coq 8.11.0
  opam install coq coq-ext-lib
  # install iris
  git clone https://gitlab.mpi-sws.org/iris/iris.git
  (cd iris && git reset --hard 62be0a86890dbbf0dd3e4fc09edaa6d0227baebd && make build-dep && make -j3 && make install)
  # install cpp2v
  git clone https://gitlab.com/bedrocksystems/cpp2v.git
  (cd cpp2v && make cpp2v cpp2v_plugin coq && make install)
  ```

  ### OSX

  ```sh
  brew install llvm cmake opam
  export PATH=/usr/local/opt/llvm/bin:${PATH}
  # install opam dependencies
  opam repo add coq-released https://coq.inria.fr/opam/released
  opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
  opam pin coq 8.11.0
  opam install coq coq-ext-lib
  # install iris
  git clone https://gitlab.mpi-sws.org/iris/iris.git
  (cd iris && git reset --hard 62be0a86890dbbf0dd3e4fc09edaa6d0227baebd && make build-dep && make -j3 && make install)
  # install cpp2v
  git clone https://gitlab.com/bedrocksystems/cpp2v.git
  cd cpp2v
  mkdir build && cd build
  cmake -D CMAKE_EXE_LINKER_FLAGS=-L/usr/local/opt/llvm/lib ..
  cmake --build . --target cpp2v
  cd ..
  make coq
  ```

  ## Examples
  See the examples in the `tests` directory.
  More examples will be added as the feature set evolves.

  You can run the tests with:

  ```sh
  $ make test
  ```

  ## Documentation
  https://bedrocksystems.gitlab.io/cpp2v/
  Coq sources for the documentation are in `doc/`

  ## Repository Layout

  - The implementation of the `cpp2v` tool is in `src` and `include`.
  - The definition of the accompanying Coq data types is in `theories/lang/cpp/syntax` directory. The notation in `theories/lang/cpp/parser.v` is used to setup the environment for the generated code.
  - The axiomatic semantics of the abstract syntax tree is defined in the `theories/lang/cpp/logic` directory.
---