I am using this template repository for my Coq project. There is something wrong with this project's
theories/dune is like this. It lacks
name. How can I fill it out with something? If I leave it blank,
dune build errs. Perhaps, I need to generate files from
meta.yml only once and I don't have to care about it?
; This file was generated from `meta.yml`, please do not edit manually. ; Follow the instructions on https://github.com/coq-community/templates to regenerate. (coq.theory (name ) (package coq-short) (synopsis "synopsis"))
@pikachu the name part is filled in from the
namespace field in
shortname: huffman namespace: Huffman synopsis: Coq proof of the correctness of the Huffman coding algorithm
(coq.theory (name Huffman) (package coq-huffman) (synopsis "Coq proof of the correctness of the Huffman coding algorithm"))
Do you know where the document of
meta.yml exists? I found some examples but couldn't find its specifications.
@pikachu the best documentation we have is a yaml file in the template repo: https://github.com/coq-community/templates/blob/master/ref.yml
However, it usually doesn't specify exactly how a
meta.yml field is used, just where (in what template files)
so looking at the
.mustache files can be the best available documentation in some cases
I really appreciate your comment!
I will refer to it in the future.
Karl Palmskog has marked this topic as resolved.
Last updated: Oct 04 2023 at 19:01 UTC