From a201fdad40ca0034dc752428a221be0e03776fa5 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Thu, 14 Nov 2024 14:00:36 +0100
Subject: [PATCH] modify meta.yml and generate README.md for new building
 instructions

---
 README.md | 13 ++++++++++---
 meta.yml  | 28 ++++++++++++++++++++++++++++
 2 files changed, 38 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index c317c4c..cdc7d61 100644
--- a/README.md
+++ b/README.md
@@ -48,14 +48,22 @@ basic plane topology definitions, and a theory of combinatorial hypermaps.
 ## Building and installation instructions
 
 The easiest way to install the latest released version of The Four Color Theorem
-is via [OPAM](https://opam.ocaml.org/doc/Install.html):
+is via [opam](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam install coq-fourcolor
 ```
 
-To instead build and install manually, do:
+If you are only interested in the formalization of real numbers, you can install
+it separately:
+
+```shell
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam install coq-fourcolor-reals
+```
+
+To instead build and install the whole project manually from the repository, do:
 
 ``` shell
 git clone https://github.com/coq-community/fourcolor.git
@@ -64,7 +72,6 @@ make   # or make -j <number-of-cores-on-your-machine>
 make install
 ```
 
-
 ## Documentation
 
 The [Four Color Theorem](https://en.wikipedia.org/wiki/Four_color_theorem) (Appel & Haken, 1976) is a landmark result of graph theory.
diff --git a/meta.yml b/meta.yml
index e84bc28..bbd2f5f 100644
--- a/meta.yml
+++ b/meta.yml
@@ -85,6 +85,34 @@ keywords:
 categories:
 - name: Mathematics/Combinatorics and Graph Theory
 
+build: |-
+  ## Building and installation instructions
+  
+  The easiest way to install the latest released version of The Four Color Theorem
+  is via [opam](https://opam.ocaml.org/doc/Install.html):
+  
+  ```shell
+  opam repo add coq-released https://coq.inria.fr/opam/released
+  opam install coq-fourcolor
+  ```
+
+  If you are only interested in the formalization of real numbers, you can install
+  it separately:
+
+  ```shell
+  opam repo add coq-released https://coq.inria.fr/opam/released
+  opam install coq-fourcolor-reals
+  ```
+  
+  To instead build and install the whole project manually from the repository, do:
+  
+  ``` shell
+  git clone https://github.com/coq-community/fourcolor.git
+  cd fourcolor
+  make   # or make -j <number-of-cores-on-your-machine> 
+  make install
+  ```
+
 documentation: |-
   ## Documentation