Added notes about Guix profiles and Rocq packaging.

Change-Id: Iebd4ec69d1d48bad9d7369a8512b289a5f53569f

1 files changed, 54 insertions, 0 deletions

diff --git a/profiles.org b/profiles.org
new file mode 100644
index 00000000000..18f4f516c7c
--- /dev/null
+++ b/profiles.org
@@ -0,0 +1,54 @@
+* Profiles
+
+** What is a profile?
+
+A profile is a directory of symlinks which point to the paths of built
+artifacts in the store.
+
+** How do the paths of a system get set in a shell?
+
+In your bash profile. When you open a shell, bash profile source's
+$GUIX/etc/profile. This sets the path.
+
+These profiles are themselves derivations. Your guix profile is a directory
+built as a derivation, and your home directory simply points to it.
+
+For more details, see (guix profiles)
+
+** What is an input in a package?
+
+An package "input" is a package dependency it is necessary to build or use the
+package.
+
+** What is a propagated input in a package?
+
+A "propagated input" is a package dependency that gets added to the
+profile. It is useful for specifying runtime dependencies.
+
+The "propogated inputs" of a package are used to build profiles
+recursively. The specify the paths that get added to a profile.
+
+** What is a native input in a package?
+
+A "native input" is a build dependency on the build architecture. It could be
+different than the target architecture in a cross compilation.
+
+** What is an input in a derivation?
+
+The inputs of a derivation are its runtime dependencies.
+
+** How does "hash guix" work?
+
+...
+
+** What do you want the Rocq packaging to look like?
+
+Specify each package individually. Rocq's keystone package is "rocq-runtime"
+so it should be installed first and labelled as such. For each of the other
+packages, make sure that you inherit "rocq-runtime" and extend them as
+necessary.
+
+Give clear descriptions of the packages you build.
+
+Make sure the propogated inputs are "sticky", so that all dependent propogated
+inputs get bubbled up to the profile.