-
Notifications
You must be signed in to change notification settings - Fork 38
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #1021 from AdaCore/updates_for_blog_post
Python script to generate a rules file from the RST files
- Loading branch information
Showing
5 changed files
with
403 additions
and
0 deletions.
There are no files selected for viewing
20 changes: 20 additions & 0 deletions
20
content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/Makefile
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
# Minimal makefile for Sphinx documentation | ||
# | ||
|
||
# You can set these variables from the command line, and also | ||
# from the environment for the first two. | ||
SPHINXOPTS ?= | ||
SPHINXBUILD ?= sphinx-build | ||
SOURCEDIR = . | ||
BUILDDIR = build | ||
|
||
# Put it first so that "make" without argument is like "make help". | ||
help: | ||
@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) | ||
|
||
.PHONY: help Makefile | ||
|
||
# Catch-all target: route all unknown targets to Sphinx using the new | ||
# "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS). | ||
%: Makefile | ||
@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) |
105 changes: 105 additions & 0 deletions
105
content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/README.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,105 @@ | ||
# Guidelines for Safe and Secure Ada/SPARK | ||
|
||
Customizable coding standards maintenance and generation. | ||
|
||
## Introduction | ||
|
||
This folder contains all the necessary content necessary to generate | ||
a coding standard for use in any size software project. The default | ||
content is a good starting point, but most users will want to customize | ||
the standards to fit their own needs and coding styles. | ||
|
||
In addition, many of the standards we want to enforce could be verified | ||
automatically with a static analysis tool. This repository assumes the | ||
`GNATcheck` tool will be used. Most of the standards contain the specific | ||
rule that would be used to verify compliance. | ||
|
||
This README file contains instructions on how to customize content | ||
and build your own coding standards document. | ||
|
||
## Prerequisites | ||
|
||
### Sphinx | ||
|
||
The only tool actually required for building your document is the | ||
Sphinx utilities located [here](https://www.sphinx-doc.org/). Once | ||
downloaded and installed, most of the output formats created by | ||
Sphinx will be available. For formats that require additional tools, | ||
please see the Sphinx documentation | ||
|
||
### GNATcheck | ||
|
||
`GNATcheck` is part of the Static Analysis Suite provided by **AdaCore**. | ||
It is designed as a coding standards checker, and comes with many | ||
pre-defined rules to use in validating standards conformance. In | ||
addition, it uses the **Langkit Query Language** to allow users to | ||
define their own rules. | ||
|
||
### Python | ||
|
||
You will notice that many of the individual coding standards specify | ||
the verification method as **GNATcheck rule**. For these methods, | ||
a particular `GNATcheck` rule is specified, using the RST role **rule** | ||
to identify formatting for the rule. In the **tools** folder is a | ||
python script **generate_rules_file.py** that can be used to build | ||
a rules input file for `GNATcheck`. To use that script, you would | ||
obviously need to install a version of Python (3.9 or better should work). | ||
|
||
### make (Linux only) | ||
|
||
If you are running this in a Linux environment, the build process | ||
uses a **Makefile**, so you do need to have **make** on your path. | ||
|
||
## Modifying the Content | ||
|
||
The content files are all written in ReStructured Text (RST). For | ||
those not familiar, a good "cheat sheet" can be found at the | ||
Docutils site on SourceForge | ||
[here](https://docutils.sourceforge.io/docs/ref/rst/directives.html). | ||
The most likely candidate for modifications is the **chapters/guidelines** | ||
folder. | ||
|
||
### Adding a New Standard | ||
|
||
For each guideline subsection, there is an RST file and a subfolder. | ||
To add a new standard, first go into the subfolder and create a new file for | ||
your standard. Feel free to use any of the other files as a template! Then, | ||
edit the subsection RST file to include your new standard file in the | ||
*.toctree* structure. That’s it – just rebuild the document and you’ve added | ||
your standard! | ||
|
||
If your new standard is detectable using a `GNATcheck` rule, make sure you | ||
set the Verification Method field in your standard to indicate | ||
`GNATcheck`, and which rule it needs to verify the standard. For example: | ||
|
||
``` | ||
GNATcheck rule: :rule:`OTHERS_In_CASE_Statements` | ||
``` | ||
|
||
### Adding a New Programming Practice Category | ||
|
||
If you want to add a whole new sub-collection of standards, the process | ||
is similar. Now, in the **guidelines** folder you need to add an RST | ||
file and subfolder, and populate them appropriately. (Again, copy-and-paste | ||
is the best way to get started.) The extra step here is you need to modify | ||
the *.toctree* structure in the **index.rst** file (located in the document's | ||
main directory) and add your new subsection. | ||
|
||
## Building Your Document | ||
|
||
Once you have made your modifications, building the document is easy! | ||
Go into the document's main directory and type `make <format>` where | ||
`<format>` is one of the allowed formats. Typing `make` with no | ||
format will give you a list of all available formats. Note that | ||
this will work on Windows as well as Linux - there is a file **make.bat** | ||
that works on Windows, and a **Makefile** that works on Linux. | ||
|
||
Output will be placed in the **build** directory (which will be created | ||
if it does not exist). | ||
|
||
### Customizing your build process | ||
|
||
The **make** files are designed to simplify the build process. If you are | ||
more familiar with the Sphinx build process, you can either edit those files | ||
to add your own options, or call `sphinx-build` directly with the | ||
appropriate options. |
90 changes: 90 additions & 0 deletions
90
content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/conf.py
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,90 @@ | ||
# Configuration file for the Sphinx documentation builder. | ||
# | ||
# This file only contains a selection of the most common options. For a full | ||
# list see the documentation: | ||
# https://www.sphinx-doc.org/en/master/usage/configuration.html | ||
|
||
# -- Path setup -------------------------------------------------------------- | ||
|
||
# If extensions (or modules to document with autodoc) are in another directory, | ||
# add these directories to sys.path here. If the directory is relative to the | ||
# documentation root, use os.path.abspath to make it absolute, like shown here. | ||
# | ||
# import os | ||
# import sys | ||
# sys.path.insert(0, os.path.abspath('.')) | ||
|
||
|
||
# -- Project information ----------------------------------------------------- | ||
|
||
project = 'Coding Standards' | ||
copyright = '2024, AdaCore Technologies' | ||
author = 'AdaCore Technologies' | ||
|
||
|
||
# -- General configuration --------------------------------------------------- | ||
|
||
# Add any Sphinx extension module names here, as strings. They can be | ||
# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom | ||
# ones. | ||
extensions = [ | ||
'sphinx.ext.extlinks', | ||
] | ||
|
||
# Add any paths that contain templates here, relative to this directory. | ||
templates_path = ['_templates'] | ||
|
||
# List of patterns, relative to source directory, that match files and | ||
# directories to ignore when looking for source files. | ||
# This pattern also affects html_static_path and html_extra_path. | ||
exclude_patterns = [] | ||
|
||
# sphinx.ext.extlinks: markup to shorten external links | ||
extlinks = { | ||
'arm': ('http://www.ada-auth.org/standards/12rm/html/RM-%s.html', | ||
'[Ada Reference Manual; section %s]'), | ||
'aarm': ('http://www.ada-auth.org/standards/12aarm/html/AA-%s.html', | ||
'[Annotated Ada Reference Manual; section %s]'), | ||
'arm22': ('http://www.ada-auth.org/standards/22rm/html/RM-%s.html', | ||
'[Ada Reference Manual; section %s]'), | ||
'aarm22': ('http://www.ada-auth.org/standards/22aarm/html/AA-%s.html', | ||
'[Annotated Ada Reference Manual; section %s]'), | ||
'rat05': ('https://www.adaic.org/resources/add_content/standards/05rat/html/Rat-%s.html', | ||
'[Rationale for Ada 2005; section %s]'), | ||
'rat12': ('http://www.ada-auth.org/standards/12rat/html/Rat12-%s.html', | ||
'[Rationale for Ada 2012; section %s]'), | ||
'wikipedia': ('https://en.wikipedia.org/wiki/%s', | ||
'[Wikipedia page: %s]'), | ||
'spark_ug': ('https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/en/%s.html', | ||
'[SPARK User\'s Guide: %s]'), | ||
'spark_ugs': ('https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/en/source/%s', | ||
'[SPARK User\'s Guide: %s]'), | ||
'spark_rm': ('https://docs.adacore.com/spark2014-docs/html/lrm/%s.html', | ||
'[SPARK Reference Manual: %s]'), | ||
'spark_rm_url': ('https://docs.adacore.com/spark2014-docs/html/lrm/%s', | ||
'[SPARK Reference Manual: %s]'), | ||
'gnat_ugn': ('https://docs.adacore.com/gnat_ugn-docs/html/gnat_ugn/gnat_ugn/%s.html', | ||
'[GNAT User\'s Guide for Native Platforms: %s]'), | ||
'gnat_ugn_url': ('https://docs.adacore.com/gnat_ugn-docs/html/gnat_ugn/gnat_ugn/%s', | ||
'[GNAT User\'s Guide for Native Platforms: %s]'), | ||
'gnat_rm': ('https://docs.adacore.com/live/wave/gnat_rm/html/gnat_rm/%s.html', | ||
'[GNAT Reference Manual: %s]'), | ||
'gnat_rm_url': ('https://docs.adacore.com/live/wave/gnat_rm/html/gnat_rm/%s', | ||
'[GNAT Reference Manual: %s]'), | ||
'gnat_check_rm_url': ('https://docs.adacore.com/live/wave/lkql/html/gnatcheck_rm/gnatcheck_rm/%s', | ||
'[GNATcheck Reference Manual: %s]'), | ||
'gnat_stack_ug_url': ('http://docs.adacore.com/live/wave/gnatstack/html/gnatstack_ug/%s', | ||
'[GNATstack User\'s Guide: %s]'), | ||
} | ||
|
||
# -- Options for HTML output ------------------------------------------------- | ||
|
||
# The theme to use for HTML and HTML Help pages. See the documentation for | ||
# a list of builtin themes. | ||
# | ||
html_theme = 'alabaster' | ||
|
||
# Add any paths that contain custom static files (such as style sheets) here, | ||
# relative to this directory. They are copied after the builtin static files, | ||
# so a file named "default.css" will overwrite the builtin "default.css". | ||
html_static_path = ['_static'] |
35 changes: 35 additions & 0 deletions
35
content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/make.bat
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
@ECHO OFF | ||
|
||
pushd %~dp0 | ||
|
||
REM Command file for Sphinx documentation | ||
|
||
if "%SPHINXBUILD%" == "" ( | ||
set SPHINXBUILD=sphinx-build | ||
) | ||
set SOURCEDIR=. | ||
set BUILDDIR=build | ||
|
||
if "%1" == "" goto help | ||
|
||
%SPHINXBUILD% >NUL 2>NUL | ||
if errorlevel 9009 ( | ||
echo. | ||
echo.The 'sphinx-build' command was not found. Make sure you have Sphinx | ||
echo.installed, then set the SPHINXBUILD environment variable to point | ||
echo.to the full path of the 'sphinx-build' executable. Alternatively you | ||
echo.may add the Sphinx directory to PATH. | ||
echo. | ||
echo.If you don't have Sphinx installed, grab it from | ||
echo.http://sphinx-doc.org/ | ||
exit /b 1 | ||
) | ||
|
||
%SPHINXBUILD% -M %1 %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O% | ||
goto end | ||
|
||
:help | ||
%SPHINXBUILD% -M help %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O% | ||
|
||
:end | ||
popd |
Oops, something went wrong.