Fixes #3659 I was testing serve_header.py with my local development setup and noticed that when I moved directories into or out of the monitored root, they weren't being picked up properly. The script would only detect create and delete events but not move operations. This was happening because the on_any_event handler only checked for 'created' and 'deleted' events on directories. Move events have a separate event type 'moved' that includes both the source and destination paths. The fix treats a move event like a combination of delete (for the source) and create (for the destination) - we rescan to remove any trees that were moved out, and add the destination directory to check for new trees that were moved in. This should make the development workflow smoother when reorganizing project directories while the server is running. Signed-off-by: Samaresh Kumar Singh <ssam3003@gmail.com>
serve_header.py
Serves the single_include/nlohmann/json.hpp header file over HTTP(S).
The header file is automatically amalgamated on demand.
Prerequisites
-
Make sure these Python packages are installed.
PyYAML watchdog(see
tools/serve_header/requirements.txt) -
To serve the header over HTTPS (which is required by Compiler Explorer at this time), a certificate is needed. The recommended method for creating a locally trusted certificate is to use
mkcert.- Install the
mkcertcertificate authority into your trust store(s):$ mkcert -install - Create a certificate for
localhost:The command will create two files,$ mkcert localhostlocalhost.pemandlocalhost-key.pem, in the current working directory. It is recommended to create them in the top level or project root directory.
- Install the
Usage
serve_header.py has a built-in default configuration that will serve the single_include/nlohmann/json.hpp header file relative to the top level or project root directory it is homed in.
The built-in configuration expects the certificate localhost.pem and the private key localhost-key.pemto be located in the top level or project root directory.
To start serving the json.hpp header file at https://localhost:8443/json.hpp, run this command from the top level or project root directory:
$ make serve_header
Open Compiler Explorer and try it out:
#include <https://localhost:8443/json.hpp>
using namespace nlohmann;
#include <iostream>
int main() {
// these macros are dynamically injected into the header file
std::cout << JSON_BUILD_TIME << " (" << JSON_BUILD_COUNT << ")\n";
return 0;
}
serve_header.pydynamically injects the macrosJSON_BUILD_COUNTandJSON_BUILD_TIMEinto the served header file. By comparing build count or time output from the compiled program with the output fromserve_header.py, one can be reasonably sure the compiled code uses the expected revision of the header file.
Configuration
serve_header.py will try to read a configuration file serve_header.yml in the top level or project root directory, and will fall back on built-in defaults if the file cannot be read.
An annotated example configuration can be found in tools/serve_header/serve_header.yml.example.
Serving json.hpp from multiple project directory instances or working trees
serve_header.py was designed with the goal of supporting multiple project roots or working trees at the same time.
The recommended directory structure is shown below but serve_header.py can work with other structures as well, including a nested hierarchy.
json/ ⮜ the parent or web server root directory
├── develop/ ⮜ the main git checkout
│ └── ...
├── feature1/
│ └── ... any number of additional
├── feature2/ ⮜ working trees (e.g., created
│ └── ... with git worktree)
└── feature3/
└── ...
To serve the header of each working tree at https://localhost:8443/<worktree>/json.hpp, a configuration file is needed.
-
Create the file
serve_header.ymlin the top level or project root directory of any working tree:root: ..By shifting the web server root directory up one level, the
single_include/nlohmann/json.hppheader files relative to each sibling directory or working tree will be served. -
Start
serve_header.pyby running this command from the same top level or project root directory the configuration file is located in:$ make serve_header
serve_header.py will automatically detect the addition or removal of working trees anywhere within the configured web server root directory.
