I am using this template repository for my Coq project. There is something wrong with this project's meta.yml
.
<https://github.com/diohabara/coq-template>
The auto-generated 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 meta.yml
for example:
shortname: huffman
namespace: Huffman
synopsis: Coq proof of the correctness of the Huffman coding algorithm
yields
(coq.theory
(name Huffman)
(package coq-huffman)
(synopsis "Coq proof of the correctness of the Huffman coding algorithm"))
@Karl Palmskog
Thank you!
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
@Karl Palmskog
I really appreciate your comment!
I will refer to it in the future.
Karl Palmskog has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC