Merge branch 'main' into melange/error-out-melc-missing

* main:
  test(melange): demonstrate error in melange compilation trying to build @ALL (ocaml#6485)
  chore(nix): make it faster to get melange (ocaml#6347)
  refactor: status db style tweaks (ocaml#6478)
  fix: improve error message for status db (ocaml#6479)
  refactor: remove unused [flags] parameter (ocaml#6480)
  refactor(ctypes): remove pesky aliases (ocaml#6482)
  chore: tweak `hacking.rst` following `dune.exe` move to _boot (ocaml#6484)
  feature(coq): automatic detection of native
  chore(coq): bump Coq lang to 0.7
  test: disable formatting for a single dune file (ocaml#6465)
  refactor: clean up module compilation (ocaml#6461)
  doc: add button to copy code blocks in Dune manual (ocaml#6428)
  refactor: deforest a set conversion (ocaml#6473)
  refactor: remove temporary map used for sorting (ocaml#6472)
  fix(melange): handle include_subdirs unqualified (ocaml#6475)

.readthedocs.yaml

@@ -0,0 +1,13 @@
+version: 2
+
+build:
+  os: "ubuntu-22.04"
+  tools:
+    python: "3.10"
+
+sphinx:
+  configuration: doc/conf.py
+
+python:
+  install:
+    - requirements: doc/requirements.txt

CHANGES.md

@@ -1,3 +1,10 @@
+Unreleased
+----------
+
+- Coq native mode is now automatically detected by Dune starting with Coq lang
+  0.7. `(mode native)` has been deprecated in favour of detection from the
+  configuration of Coq. (#6409, @Alizter)
+
 3.6.0 (2022-11-14)
 ------------------
 

Makefile

@@ -134,7 +134,7 @@ distclean: clean
 doc:
 	sphinx-build -W doc doc/_build
 
-# livedoc-deps: you may need to [pip3 install sphinx-autobuild] and [pip3 install sphinx-rtd-theme]
+# livedoc-deps: you may need to [pip3 install sphinx-autobuild] and [pip3 install -r doc/requirements.txt]
 livedoc:
 	cd doc && sphinx-autobuild . _build --port 8888 -q --re-ignore '\.#.*'
 

doc/conf.py

@@ -31,7 +31,9 @@
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
-extensions = []
+extensions = [
+    'sphinx_copybutton'
+]
 
 # Add any paths that contain templates here, relative to this directory.
 templates_path = ['_templates']

doc/coq.rst

@@ -142,19 +142,15 @@ The semantics of the fields are:
   You may still use installed libraries in your Coq project, but there is
   currently no way for Dune to know about it.
 
-- You can enable the production of Coq's native compiler object files by setting
-  ``<coq_native_mode>`` to ``native``. This passes ``-native-compiler on`` to
-  Coq and install the corresponding object files under ``.coq-native``, when in
-  the ``release`` profile. The regular ``dev`` profile skips native compilation
-  to make the build faster. This has been available since :ref:`Coq lang
-  0.3<coq-lang>`.
-
-  Please note: support for ``native_compute`` is **experimental** and requires a
-  version of Coq later than 8.12.1. Furthermore, dependent theories *must* be
-  built with the ``(mode native)`` enabled. In addition to that, Coq must be
-  configured to support native compilation. Dune explicitly disables the
-  generation of native compilation objects when ``(mode vo)`` is enabled,
-  irrespective of the configuration of Coq. This will be improved in the future.
+- From version :ref:`Coq lang 0.7<coq-lang>` onwards, if Coq has been configured
+  with ``-native-compiler yes`` or ``ondemand``, Dune will always build the
+  ``cmxs`` files together with the ``vo`` files.
+
+  You may override this by specifying ``(mode native)`` or ``(mode vo)``. Before
+  :ref:`Coq lang 0.7<coq-lang>`, the native mode had to be manually specified.
+
+  Previous versions of Dune before 3.7 would disable the native rules depending
+  on whether or not the ``dev`` profile was selected.
 
 Coq Documentation
 ~~~~~~~~~~~~~~~~~
@@ -249,8 +245,12 @@ The supported Coq language versions (not the version of Coq) are:
 - ``0.3``: Support for ``(mode native)`` requires Coq >= 8.10 (and Dune >= 2.9
   for Coq >= 8.14).
 - ``0.4``: Support for interproject composition of theories.
-- ``0.5``: ``(libraries ...)`` field deprecated in favor of ``(plugins ...)`` field.
+- ``0.5``: ``(libraries ...)`` field deprecated in favor of ``(plugins ...)``
+  field.
 - ``0.6``: Support for ``(stdlib no)``.
+- ``0.7``: ``(mode )`` is automatically detected from the configuration of Coq
+  and ``(mode native)`` is deprecated. The ``dev`` profile also no longer
+  disables native compilation.
 
 .. _coq-lang-1.0:
 

doc/hacking.rst

@@ -22,8 +22,9 @@ file is automatically updated during development when we modify the ``dune``
 files in the repository. ``boot/duneboot.ml`` itself is built with a single
 invocation of ``ocamlopt`` or ``ocamlc`` via the ``bootstrap.ml`` OCaml script.
 
-``boot/duneboot.ml`` builds a ``dune.exe`` binary at the root of the source tree
-and uses this binary to build everything else.
+``boot/duneboot.ml`` builds a ``dune.exe`` binary in the ``_boot`` directory
+and uses this binary to build everything else. As a convenience, ``dune.exe``
+at the root of the source tree executes this binary.
 
 ``$ make dev`` takes care of bootstrapping if needed, but if you want to just
 run the bootstrapping step itself, build the ``dune.exe`` target with

doc/requirements.txt

@@ -0,0 +1,3 @@
+sphinx >= 4.5.0
+sphinx_rtd_theme >= 1.0.0
+sphinx-copybutton >= 0.5.0