Propagate KaRaMeL renaming to book/

book/AdvancedTopics.rst

@@ -1,4 +1,4 @@
-Advanced KreMLin topics
+Advanced KaRaMeL topics
 =======================
 
 Bundling
@@ -32,7 +32,7 @@ file is ``N₁_..._Nₙ``, but can be controlled by appending an optional
   places. This would cause errors with conflicting symbols at link-time, and
   would have a disastrous impact on your code segment size. Bundles do not
   change the fact that a definition only appears in a single place for each
-  kremlin invocation.
+  KaRaMeL invocation.
 
 
 Bundles for hiding implementation details
@@ -72,7 +72,7 @@ as follows:
 
 .. note::
 
-  Since KreMLin automatically eliminates unreachable definitions by default,
+  Since KaRaMeL automatically eliminates unreachable definitions by default,
   bundling oftentimes prunes the call-graph quite heavily and is used to remove
   definitions that would otherwise be unreachable.
 
@@ -111,7 +111,7 @@ spec). If a declaration is not eliminated as expected, use ``-d reachability``
 which will explain why a declaration is still reachable and, therefore, not
 marked as private.
 
-Separate compilation via KreMLin
+Separate compilation via KaRaMeL
 --------------------------------
 
 This sections covers authoring two different projects that are built, extracted to
@@ -132,22 +132,22 @@ In particular, this means that if project B (e.g. miTLS) depends on project A
   ``--already_cached``) and compiled to ``liba.a`` (via suitable ``make``
   checks)
 - project B must ensure that no linker symbols from project A are generated as
-  part of its build (using kremlin's ``-library`` option)
+  part of its build (using KaRaMeL's ``-library`` option)
 - project B will regenerate headers for declarations from within project A that
   will be used by project A: this is the declaration from B, as seen from
   project A; see as an example ``mitls-fstar/src/tls/dist/compact/EverCrypt.h``
 
 The last point means that project B will *never* include a header that was
 generated via the build of project A.
 
-The reason for doing so is related to monomorphization. Since kremlin does not
+The reason for doing so is related to monomorphization. Since KaRaMeL does not
 dump information from project A to project B, project A may contain a copy of,
 say, ``K__int32__int32`` (the type of pairs monomorphized to ``int32``). When
-compiling project B, however, kremlin does not know that this pair has already
+compiling project B, however, KaRaMeL does not know that this pair has already
 been monomorphized and may generate a second monomorphization of it in project
 B, resulting in C name conflicts and compilation errors if you try to mix
-headers from the kremlin run of A with the kremlin run of B. *Never mix headers
-obtained from different runs of kremlin!*
+headers from the KaRaMeL run of A with the KaRaMeL run of B. *Never mix headers
+obtained from different runs of KaRaMeL!*
 
 Via static headers
 ^^^^^^^^^^^^^^^^^^
@@ -158,7 +158,7 @@ exclusively as a set of static headers, i.e. headers that contain definitions
 marked as ``inline static``.
 
 In that case, project A must pass a suitable ``-static-header`` option to
-KreMLin (same syntax as ``-bundle``, ``-library``, etc.). Definitions that match
+KaRaMeL (same syntax as ``-bundle``, ``-library``, etc.). Definitions that match
 the argument will then appear in their respective header files.
 
 Project B will then need to use (in addition to ``-library``):
@@ -188,7 +188,7 @@ type (see digression above).
 
   kremlib does a mix of these two approaches; uint modules are extracted as
   static headers (and the suitable -static-header and -library options for
-  clients are hardcoded in kremlin) -- this allows projects such as HACL* to not
+  clients are hardcoded in KaRaMeL) -- this allows projects such as HACL* to not
   require any libkremlib.a; other parts of kremlib do not use this facility,
   meaning that projects like miTLS still link against libkremlib.a to find
   external symbols (e.g. from ``FStar.Date``)

book/BufferLibraries.rst

@@ -27,7 +27,7 @@ In order to manipulate const pointers, you can use ``LowStar.ConstPointer``. It
 is represented as an abstract type distinct from regular, immutable, or unitialized
 buffers (all instances of the base monotonic buffer type). Having a separate
 abstract type allows identifiying const pointers as a separate, disjoint type at
-extraction, without requiring the built-in Low* checker in KreMLin to insert
+extraction, without requiring the built-in Low* checker in KaRaMeL to insert
 casts.
 
 Injecting ``buffer`` or ``ibuffer`` into a ``const_buffer`` generates no casts

book/Core.rst

@@ -196,14 +196,14 @@ source of truth.
 Extensions to Low*
 ------------------
 
-KreMLin supports a number of programming patterns beyond the original paper
+KaRaMeL supports a number of programming patterns beyond the original paper
 formalization, which aim to maximize programmer productivity. We now review
 the main ones.
 
 Equalities monomorphization
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-One can rely on KreMLin to compile F*'s structural equality (the ``(=)``
+One can rely on KaRaMeL to compile F*'s structural equality (the ``(=)``
 operator) to C functions specialized to each type. Furthermore, the function
 below demonstrates the use of a struct type as a value, which is
 straightforwardly compiled to a C structure passed by value. Be aware that doing
@@ -229,7 +229,7 @@ so has performance implications (see ??).
 Inductives as tagged unions; pattern-matching compilation
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-One may also use F* inductives, knowing that KreMLin will compile them as
+One may also use F* inductives, knowing that KaRaMeL will compile them as
 tagged unions. There are currently five different compilation schemes for data
 types that all aim to generate C code that is "as natural" as possible:
 
@@ -275,7 +275,7 @@ scheme and generates a complete tagged union.
 Data type monomorphization
 ^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-Generally, KreMLin performs a whole-program monomorphization of
+Generally, KaRaMeL performs a whole-program monomorphization of
 parameterized data types. The example below demonstrates this, along with a
 "pretty" compilation scheme for the option type that does not involves an
 anonymous union.
@@ -323,8 +323,8 @@ anonymous union.
 Pattern matches compilation
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-Inductives are compiled by KreMLin, and so are pattern matches. Note that
-for a series of cascading if-then-elses, KreMLin has to insert a fallback
+Inductives are compiled by KaRaMeL, and so are pattern matches. Note that
+for a series of cascading if-then-elses, KaRaMeL has to insert a fallback
 else statement, both because the original F* code may be unverified and the
 pattern-matching may be incomplete, but also because the C compiler may
 trigger an error.
@@ -358,7 +358,7 @@ trigger an error.
      }
      else
      {
-       KRML_HOST_PRINTF("KreMLin abort at %s:%d\n%s\n",
+       KRML_HOST_PRINTF("KaRaMeL abort at %s:%d\n%s\n",
          __FILE__,
          __LINE__,
          "unreachable (pattern matches are exhaustive in F*)");
@@ -427,11 +427,11 @@ Non-constant globals
 ^^^^^^^^^^^^^^^^^^^^
 
 In the case that the user defines a global variable that does not compile to
-a C11 constant, KreMLin generates a "static initializer" in the special
-``kremlinit_globals`` function. If the program has a ``main``, KreMLin
+a C11 constant, KaRaMeL generates a "static initializer" in the special
+``kremlinit_globals`` function. If the program has a ``main``, KaRaMeL
 automatically prepends a call to ``kremlinit_globals`` in the ``main``. If
 the program does not have a ``main`` and is intended to be used as a
-library, KreMLin emits a warning, which is fatal by default.
+library, KaRaMeL emits a warning, which is fatal by default.
 
 .. code:: fstar
 
@@ -459,7 +459,7 @@ library, KreMLin emits a warning, which is fatal by default.
 Code quality improvements
 -------------------------
 
-In addition to all the features describe above, KreMLin will go great lengths to
+In addition to all the features describe above, KaRaMeL will go great lengths to
 generate readable code. Here are some of the optimization passes performed.
 
 Unused argument elimination
@@ -485,14 +485,14 @@ Temporary variable elimination
 
 F* introduces a significant amount of temporary variables called ``uu___``,
 owing to its monadic let semantics. (You can see these variables looking at the
-generated OCaml code.) KreMLin uses two different syntactic criteria to get rid
+generated OCaml code.) KaRaMeL uses two different syntactic criteria to get rid
 of those.
 
 Tuple elimination
 ^^^^^^^^^^^^^^^^^
 
 To avoid allocating too many intermediary values of monomorphized tuple types,
-KreMLin applies the following two rules before data type compilation &
+KaRaMeL applies the following two rules before data type compilation &
 monomorphization:
 
 .. code::
@@ -542,7 +542,7 @@ Low*.
 The example below cannot be compiled for the following reasons:
 
 - local recursive let-bindings are not Low*;
-- local closure captures variable in scope (KreMLin does not do closure conversion)
+- local closure captures variable in scope (KaRaMeL does not do closure conversion)
 - the list type is not Low*.
 
 .. code:: fstar
@@ -566,15 +566,15 @@ to generate a ``.krml`` file.
 .. code:: bash
 
    $ krml -skip-compilation -verbose LowStar.fst
-   ⚙ KreMLin auto-detecting tools.
+   ⚙ KaRaMeL auto-detecting tools.
    (...)
    ✔ [F*,extract]
    <dummy>(0,0-0,0): (Warning 250) Error while extracting LowStar.filter_map
-   to KreMLin (Failure("Internal error: name not found aux\n"))
+   to KaRaMeL (Failure("Internal error: name not found aux\n"))
 
 To explain why the list type cannot be compiled to C, consider the snippet
 below. Data types are compiled as flat structures in C, meaning that the
-list type would have infinite size in C. This is compiled by KreMLin but
+list type would have infinite size in C. This is compiled by KaRaMeL but
 rejected by the C compiler. See ?? for an example of a linked list.
 
 .. code:: fstar
@@ -592,14 +592,14 @@ C compiler to generate a ``.o`` file.
 .. code:: bash
 
    $ krml -skip-linking -verbose LowStar.fst
-   ⚙ KreMLin auto-detecting tools.
+   ⚙ KaRaMeL auto-detecting tools.
    (...)
    ✘ [CC,./LowStar.c]
    In file included from ./LowStar.c:8:0:
    ./LowStar.h:95:22: error: field ‘tl’ has incomplete type
       LowStar_list_int32 tl;
 
-Polymorphic assumes are also not compiled. KreMLin could generate one C
+Polymorphic assumes are also not compiled. KaRaMeL could generate one C
 ``extern`` declaration per monomorphic use, but this would require the user
 to provide a substantial amount of manually-written code, so instead we
 refuse to compile the definition below.
@@ -616,14 +616,14 @@ to generate a ``.krml`` file.
 .. code:: bash
 
    $ krml -skip-compilation -verbose LowStar.fst
-   ⚙ KreMLin auto-detecting tools.
+   ⚙ KaRaMeL auto-detecting tools.
    (...)
    ✔ [F*,extract]
-   Not extracting LowStar.pair_up to KreMLin (polymorphic assumes are not supported)
+   Not extracting LowStar.pair_up to KaRaMeL (polymorphic assumes are not supported)
 
 One point worth mentioning is that indexed types are by default not
-supported. See section ?? for an unofficial KreMLin extension that works in
-some very narrow cases, or rewrite your code to make ``t`` an inductive. KreMLin
+supported. See section ?? for an unofficial KaRaMeL extension that works in
+some very narrow cases, or rewrite your code to make ``t`` an inductive. KaRaMeL
 currently does not have support for untagged unions, i.e. automatically
 making ``t`` a C union.
 
@@ -660,7 +660,7 @@ Trying to compile the snippet above will generate invalid C code.
          }
        default:
          {
-           KRML_HOST_PRINTF("KreMLin incomplete match at %s:%d\n", __FILE__, __LINE__);
+           KRML_HOST_PRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__, __LINE__);
            KRML_HOST_EXIT(253U);
          }
      }