Stream: Coq users

Topic: ✔ What's wrong with my `meta.yml`?


view this post on Zulip pikachu (Dec 28 2022 at 09:04):

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"))

view this post on Zulip Karl Palmskog (Dec 28 2022 at 09:07):

@pikachu the name part is filled in from the namespace field in meta.yml

view this post on Zulip Karl Palmskog (Dec 28 2022 at 09:09):

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"))

view this post on Zulip pikachu (Dec 28 2022 at 09:10):

@Karl Palmskog
Thank you!
Do you know where the document of meta.yml exists? I found some examples but couldn't find its specifications.

view this post on Zulip Karl Palmskog (Dec 28 2022 at 09:14):

@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)

view this post on Zulip Karl Palmskog (Dec 28 2022 at 09:17):

so looking at the .mustache files can be the best available documentation in some cases

view this post on Zulip pikachu (Dec 28 2022 at 12:13):

@Karl Palmskog
I really appreciate your comment!
I will refer to it in the future.

view this post on Zulip Notification Bot (Dec 29 2022 at 09:35):

Karl Palmskog has marked this topic as resolved.


Last updated: Jun 24 2024 at 12:02 UTC