Skip to content

Commit 037d1e4

Browse files
wlammendigama0
andauthored
Support doxyfile (#54)
* annotate configure.ac * update build documentation * update build.sh and move it to unstable * add a Doxyfile template * rm a line referencing Doxyfile * patch the version in Doxyfile.diff * support creating the Doxygen documentation in build.sh * update MVERSION, start adding support for Doxygen * exclude build directory from git * fix gitignore * keep folder build, but not its files * keep folder build, but not its files 2nd try * add empty build folder * provide a build.sh for CI * provide a build.sh for CI, add permissions * fix various bugs and glitches repported by Mario Carneiro * revert .gitignore settings * fix CI * fix CI * move build.dh to top dir of metamath and assume it is run from there by default * remove build directory * move build.sh * fix bash grammar * fix bash grammar * don't use uninitialized variables otherwise environment variables can change the behavior of the script * fix bash grammar 3rd try * use lowercase for local variables * top_dir and metamath_dir are the same * don't generate doc by default * separate the clean, configure, and doxygen steps * exit with error if doxygen not found * move configuration files to conventional locations * fix help text * typo * update file references in build.sh * there is no need to cd back to the original directory because shell scripts are executed in a sub-shell. It would only make a difference if you `source build.sh` and this is not the kind of script where that would be appropriate. * fix stray paste * fix getopts * suppress command file not found error * simplify Doxygen patch * fix message * add documentation location hint * no more source file copies * move config scripts to config dir * move binary to the root * fix doxygen build * fix a few glitches Co-authored-by: Wolf Lammen <[email protected]> Co-authored-by: Mario Carneiro <[email protected]>
1 parent 817b7e6 commit 037d1e4

File tree

13 files changed

+291
-90
lines changed

13 files changed

+291
-90
lines changed

.github/workflows/build.yml

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,8 @@ jobs:
1212
- uses: actions/checkout@v2
1313

1414
- name: build
15-
working-directory: build
1615
run: ./build.sh
1716

1817
- name: test
1918
working-directory: tests
20-
run: env METAMATH=../build/metamath ./run_test.sh *.in
19+
run: env METAMATH=../metamath ./run_test.sh *.in

.gitignore

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,9 @@ configure.ac2
2323
*~7
2424
*~8
2525
*~9
26-
# Doxygen related: configuration file and destination folder
27-
Doxyfile
28-
doc/doxy
2926
build/
27+
# Doxygen related: configuration file and destination folderbuild/
28+
29+
Doxyfile
30+
doxy/
3031
*.produced

src/Doxyfile.diff renamed to Doxyfile.diff

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
# think are quite usable. You can use this file directly by renaming it to
66
# Doxyfile. You can prepend its contents to your personal Doxyfile, so that the
77
# suggested values do not overwrite your settings. Or, of course, patch your
8-
# file with a subset suiting your needs.
8+
# file with a subset suiting your needs.
99

1010
# This file describes the settings to be used by the documentation system
1111
# doxygen (www.doxygen.org) for a project.
@@ -20,18 +20,19 @@
2020
# TAG += value [value, ...]
2121
# Values that contain spaces should be placed between quotes (\" \").
2222

23-
PROJECT_NAME = "metamath executable"
23+
#---------------------------------------------------------------------------
24+
# Project related configuration options
25+
#---------------------------------------------------------------------------
2426

25-
# TODO: Set to Metamath version
27+
PROJECT_NAME = "metamath executable"
2628

27-
PROJECT_NUMBER = "Metamath-version"
29+
# patched in by build.sh
30+
# PROJECT_NUMBER = "..."
2831

29-
PROJECT_BRIEF = "executable used to maintain *.mm files"
32+
PROJECT_BRIEF = "executable used to maintain *.mm files"
3033

3134
PROJECT_LOGO = "Metamath.png"
3235

33-
OUTPUT_DIRECTORY = "../doxy"
34-
3536
# disable Graphviz .dot output
3637

3738
HAVE_DOT = NO

Makefile.am

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
# This file is input to automake, that expands this high-level make description
2+
# to a Makefile containing the usual goals, and being capable of handling
3+
# portability issues.
4+
5+
SUBDIRS = src
6+
7+
# the following files are not used during build, but are distributed to users
8+
EXTRA_DIST = \
9+
LICENSE.TXT \
10+
README.TXT

build.sh

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
#!/bin/bash
2+
# create a metamath executable from scratch
3+
4+
# Change to the top folder of metamath-exe before
5+
# running this script, unless you provide the -m option.
6+
7+
# Draft version, proof of concept.
8+
9+
help_text=\
10+
'Builds all artefacts in the metamath-exe/build subfolder (if not directed
11+
otherwise). Change to the metamath-exe top folder first before running
12+
this script, or issue the -m option.
13+
14+
Possible options are:
15+
16+
-a Used by autotools. Put hyphens in the version string when used with -v
17+
-b build binary only, no reconfigure. Faster, but should not be used on first run.
18+
-c Clean the build directory.
19+
-d build documentation using Doxygen, in addition to building the executable.
20+
-h print this help and exit.
21+
-m followed by a directory: top folder of metamath-exe.
22+
Relative paths are relative to the current directory.
23+
-o followed by a directory: optionally clean directory and build all artefacts there.
24+
Relative paths are relative to the destination'"'"'s top metamath-exe directory.
25+
-v extract the version from metamath sources, print it and exit'
26+
27+
#============ evaluate command line parameters ==========
28+
29+
do_autoconf=1
30+
do_clean=0
31+
do_doc=0
32+
print_help=0
33+
version_only=0
34+
version_for_autoconf=0
35+
unset dest_dir
36+
top_dir="$(pwd)"
37+
38+
while getopts abcdhm:o:v flag
39+
do
40+
case "${flag}" in
41+
a) version_for_autoconf=1;;
42+
b) do_autoconf=0;;
43+
c) do_clean=1;;
44+
d) do_doc=1;;
45+
h) print_help=1;;
46+
m) cd "${OPTARG}" && top_dir=$(pwd);;
47+
o) dest_dir=${OPTARG};;
48+
v) version_only=1;;
49+
esac
50+
done
51+
52+
if [ $print_help -gt 0 ]
53+
then
54+
echo "$help_text"
55+
exit
56+
fi
57+
58+
#=========== setup environment =====================
59+
60+
src_dir="$top_dir/src"
61+
build_dir=${dest_dir:-"$top_dir/build"}
62+
63+
# verify we can navigate to the sources
64+
if [ ! -f "$src_dir/metamath.c" ]
65+
then
66+
echo 'This script must be run from the top folder of the metamath-exe directory.'
67+
echo 'Run ./build.sh -h for more information'
68+
exit
69+
fi
70+
71+
cd "$top_dir"
72+
73+
#========= extract the version from metamath.c =============
74+
75+
# look in metamath.c for a line matching the pattern ' #define MVERSION "<version>" '
76+
# and save the line in VERSION
77+
version=`grep '[[:space:]]*#[[:space:]]*define[[:space:]][[:space:]]*MVERSION[[:space:]][[:space:]]*"[^"]*"' "$src_dir/metamath.c"`
78+
79+
# extract the version (without quotes) from the saved line
80+
81+
# strip everything up to and including the first quote character
82+
version=${version#*\"}
83+
# strip everything from the first remaining quote character on
84+
version=${version%%\"*}
85+
86+
if [ $version_only -eq 1 ]
87+
then
88+
if [ $version_for_autoconf -eq 1 ]; then
89+
echo "$version" | tr ' ' -
90+
else
91+
echo "$version"
92+
fi
93+
exit
94+
fi
95+
96+
# clear the build directory
97+
if [ $do_clean -eq 1 ]
98+
then
99+
rm -rf "$build_dir"
100+
if [ $do_autoconf -eq 0 ]; then exit; fi
101+
fi
102+
103+
# Enter the build directory
104+
mkdir -p "$build_dir"
105+
cd "$build_dir"
106+
107+
# allow external programs easy access to the metamath version extracted from
108+
# the sources
109+
echo "$version" > metamath_version
110+
111+
#=========== run the configure.ac =====================
112+
113+
if [ $do_autoconf -eq 1 ]
114+
then
115+
cd "$top_dir"
116+
autoreconf -i
117+
118+
cd "$build_dir"
119+
"$top_dir/configure" -q
120+
fi
121+
122+
#=========== do the build =====================
123+
124+
make
125+
mv src/metamath "$top_dir"
126+
127+
#=========== run Doxygen documentation generator =====================
128+
129+
if [ $do_doc -eq 1 ]
130+
then
131+
if ! command doxygen -v &> /dev/null; then
132+
echo >&2 'doxygen not found. Cannot build documentation.'
133+
exit 1
134+
fi
135+
136+
cd "$build_dir/src"
137+
138+
# create a Doxyfile.local and use it for creation of documentation locally
139+
140+
# start with the settings given by the distribution
141+
cp "$top_dir/Doxyfile.diff" Doxyfile.local
142+
143+
# add the project version number
144+
echo "PROJECT_NUMBER = \"$version\"" >> Doxyfile.local
145+
146+
# let the users preferences always override...
147+
if [ -f "$top_dir/Doxyfile" ]
148+
then
149+
cat "$top_dir/Doxyfile" >> Doxyfile.local
150+
fi
151+
152+
# ... except for the destination directory. Force this to the build folder.
153+
echo "OUTPUT_DIRECTORY = \"$build_dir\"" >> Doxyfile.local
154+
155+
# make sure the logo is in the build directory
156+
cp --force --symbolic-link "$top_dir/doc/Metamath.png" .
157+
158+
doxygen Doxyfile.local
159+
echo "Documentation has been generated at $build_dir/html/index.html"
160+
fi

build/build.sh

Lines changed: 0 additions & 55 deletions
This file was deleted.

src/configure.ac renamed to configure.ac

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,18 @@
88
AC_PREREQ([2.65])
99

1010
# program name, version, email to report bugs
11-
AC_INIT([metamath], [0.114], [[email protected]])
11+
AC_INIT([metamath], [m4_esyscmd_s([./build.sh -va])], [[email protected]])
12+
13+
# Put auxiliary autoconf scripts in config/
14+
AC_CONFIG_AUX_DIR([config])
15+
16+
# Do not expect full GNU conformance (files like NEWS might be missing).
17+
# Minimal checks only.
18+
AM_INIT_AUTOMAKE([foreign])
1219

1320
# unique file name likely not existing outside the source tree.
1421
# catches incorrect --srcdir parameter in autoconf call.
15-
AC_CONFIG_SRCDIR([metamath.c])
22+
AC_CONFIG_SRCDIR([src/metamath.c])
1623

1724
# requires a config.h.in file, that is used as a template for a config.h,
1825
# modified according to following commands. A script created by autoconf
@@ -21,18 +28,14 @@ AC_CONFIG_SRCDIR([metamath.c])
2128
# common practise to do so.
2229
AC_CONFIG_HEADERS([config.h])
2330

24-
# Do not expect full GNU conformance (files like NEWS might be missing).
25-
# Minimal checks only.
26-
AM_INIT_AUTOMAKE([foreign])
27-
2831
# requires a Makefile.am, that is modified according to following commands.
2932
# AC_OUTPUT creates a Makefile.in based on this modifications..
30-
AC_CONFIG_FILES([Makefile])
33+
AC_CONFIG_FILES([Makefile src/Makefile])
3134

3235
# Checks for programs.
3336

3437
# add this to support the tools folder
35-
# AC_PROG_AWK
38+
# AC_PROG_AWK
3639

3740
# test existence of a C compiler
3841
AC_PROG_CC
@@ -49,7 +52,7 @@ AC_PROG_INSTALL
4952
# if a standard complient header is found.
5053
AC_CHECK_HEADERS([limits.h stdlib.h string.h])
5154

52-
# config.h: set HAVE_STDBOOL_H
55+
# config.h: set HAVE_STDBOOL_H
5356
AC_HEADER_STDBOOL
5457

5558
# Checks for typedefs, structures, and compiler characteristics.

doc/Metamath.png

490 Bytes
Loading

src/Makefile.am

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -40,12 +40,5 @@ metamath_SOURCES = \
4040
mmwtex.c \
4141
$(noinst_HEADERS)
4242

43-
44-
# the following files are not used during build, but are distributed to users
45-
EXTRA_DIST = \
46-
LICENSE.TXT \
47-
README.TXT \
48-
__README.TXT
49-
5043
# man pages for the executable´
51-
man_MANS = metamath.1
44+
dist_man_MANS = metamath.1

src/metamath.c

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,8 @@
7070
* - avoid characters from the following set, eligible for escaping in text, regular
7171
* expressions and so on like -begin of list ][`*+^$'?"{/}\ end of list-;
7272
* - use no space character other than simple space (U+0020);
73-
* - never use space characters at the beginning or at the end.
73+
* - never use space characters at the beginning or at the end;
74+
* - the length is limited to 26 characters.
7475
*/
7576
#define MVERSION "0.199.pre 29-Jan-2022"
7677
/* 0.199.pre
@@ -719,6 +720,20 @@
719720

720721
void command(int argc, char *argv[]);
721722

723+
/*! \fn int main(int argc, char *argv[])
724+
* \brief entry point of the metamath program
725+
* \param argc int number of commandline parameters
726+
* \param argv (char*)[] array of \a argc commandline parameters, followed by NULL
727+
* \return success 0 else failure
728+
*
729+
* Running metamath
730+
* ./metamath 'read set.mm' 'verify proof *'
731+
* will start main with \a argc set to 2, argv[0] to "read set.mm", argv[1]
732+
* to "verify proof *" (both without quotes) and argv[2] to NULL.
733+
* Returning 0 indicates successful completion, anything else some kind of
734+
failure.
735+
* For details see \ref https://en.cppreference.com/w/cpp/language/main_function.
736+
*/
722737
int main(int argc, char *argv[]) {
723738

724739
/* argc is the number of arguments; argv points to an array containing them */

0 commit comments

Comments
 (0)