diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..503bb91 --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +# Ignore intermediate binary files generated by the compiler process +obj/*.o +obj/*.ppu diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..e646c6a --- /dev/null +++ b/Makefile @@ -0,0 +1,76 @@ +# Makefile for Mizar + +# Target for installation +DESTDIR=/usr/local/bin +SYS=POSIX + +# Directory for sources +MIZSRC=. + +# Directories for binaries +FPCBIN=bin + +# Directories for object and unit files +FPCOBJ=obj + +# Path to Mizar units +MIZ_UNITS =base kernel usrtools libtools addtools + +# Compilers +FPC = fpc -Sdg -FE$(FPCBIN) -FU$(FPCOBJ) \ + $(addprefix -Fu$(MIZSRC)/,$(MIZ_UNITS)) + +FPCFLAGS = +#FPCFLAGS = -g -gc -gg -pg + +ADDDPR = $(wildcard $(MIZSRC)/addtools/*.dpr) + +BASEDPR = $(wildcard $(MIZSRC)/base/*.dpr) + +KERNELDPR = $(wildcard $(MIZSRC)/kernel/*.dpr) + +LIBDPR = $(wildcard $(MIZSRC)/libtools/*.dpr) + +USRDPR = $(wildcard $(MIZSRC)/usrtools/*.dpr) + +ADD_EXE = $(basename $(ADDDPR)) +BASE_EXE = $(basename $(BASEDPR)) +KERNEL_EXE = $(basename $(KERNELDPR)) +LIB_EXE = $(basename $(LIBDPR)) +USR_EXE = $(basename $(USRDPR)) + +.PHONY: all +all: dirs fpc_base fpc_kernel fpc_add fpc_lib fpc_usr + +clean: fpc_clean +fpc_clean: fpc_obj_clean fpc_bin_clean + +dirs: + mkdir -p $(FPCBIN) $(FPCOBJ) + +fpc_base: $(addprefix $(FPCBIN)/,$(BASE_EXE)) +fpc_kernel: $(addprefix $(FPCBIN)/,$(KERNEL_EXE)) +fpc_add: $(addprefix $(FPCBIN)/,$(ADD_EXE)) +fpc_lib: $(addprefix $(FPCBIN)/,$(LIB_EXE)) +fpc_usr: $(addprefix $(FPCBIN)/,$(USR_EXE)) + +fpc_obj_clean: + rm -r -f $(FPCOBJ)/* +fpc_bin_clean: + rm -r -f $(FPCBIN)/* + +# Rules for FPC +$(addprefix $(FPCBIN)/,$(BASE_EXE)): + $(FPC) $(FPCFLAGS) $(MIZSRC)/base/$(basename $(@F)).dpr +$(addprefix $(FPCBIN)/,$(KERNEL_EXE)): + $(FPC) $(FPCFLAGS) $(MIZSRC)/kernel/$(basename $(@F)).dpr +$(addprefix $(FPCBIN)/,$(ADD_EXE)): + $(FPC) $(FPCFLAGS) $(MIZSRC)/addtools/$(basename $(@F)).dpr +$(addprefix $(FPCBIN)/,$(filter-out $(SPECIAL_LIB),$(LIB_EXE))): + $(FPC) $(FPCFLAGS) $(MIZSRC)/libtools/$(basename $(@F)).dpr +$(addprefix $(FPCBIN)/,$(USR_EXE)): + $(FPC) $(FPCFLAGS) $(MIZSRC)/usrtools/$(basename $(@F)).dpr + +install: + cp bin/* $(DESTDIR)/ + cp scripts/$(SYS)/* $(DESTDIR)/ diff --git a/bin/.gitignore b/bin/.gitignore new file mode 100644 index 0000000..1aff4ce --- /dev/null +++ b/bin/.gitignore @@ -0,0 +1,4 @@ +# Ignore everything in this directory +* +# ...except for this file +!.gitignore \ No newline at end of file diff --git a/obj/.gitignore b/obj/.gitignore new file mode 100644 index 0000000..1aff4ce --- /dev/null +++ b/obj/.gitignore @@ -0,0 +1,4 @@ +# Ignore everything in this directory +* +# ...except for this file +!.gitignore \ No newline at end of file diff --git a/scripts/POSIX/miz2abs b/scripts/POSIX/miz2abs new file mode 100755 index 0000000..b3f2e9a --- /dev/null +++ b/scripts/POSIX/miz2abs @@ -0,0 +1,34 @@ +#!/bin/sh +# +# Mizar Abstractor, example shell command +# + +accommodate() +{ + accom $1 + if test "$?" = "0" + then + make_abstract $1 + else + errflag $1 + addfmsg $1 $MIZFILES/mizar + exit 2 + fi +} + +make_abstract() +{ + absedt $1 + edtfile $1 + mv $1.'$-$' $1.abs +} + +if test -z "$1" + then + echo "> `basename $0` error : Missing parameter" + echo "Usage: `basename $0` mizar_article_name" + exit 1 + else + accommodate "`dirname $1`/`basename $1 .miz`" +fi + diff --git a/scripts/POSIX/miz2prel b/scripts/POSIX/miz2prel new file mode 100755 index 0000000..bed184e --- /dev/null +++ b/scripts/POSIX/miz2prel @@ -0,0 +1,52 @@ +#!/bin/sh +# +# Mizar local data base creation, example shell command +# + +accommodate() +{ + accom $1 + if test "$?" = "0" + then + exporting $1 + else + errflag $1 + addfmsg $1 $MIZFILES/mizar + exit 2 + fi +} + +exporting() +{ + exporter $1 + if test "$?" = "0" + then + make_prel $1 + else + errflag $1 + addfmsg $1 $MIZFILES/mizar + exit 3 + fi +} + +make_prel() +{ + transfer $1 + for ext in dno dcl dco def the sch + do + if test -f "$1.$ext" + then + rm "$1.$ext" + fi + done + echo "Local data base created" +} + +if test -z "$1" + then + echo "> `basename $0` error : Missing parameter" + echo "Usage: `basename $0` mizar_article_name" + exit 1 + else + accommodate "`dirname $1`/`basename $1 .miz`" +fi diff --git a/scripts/POSIX/mizf b/scripts/POSIX/mizf new file mode 100755 index 0000000..0876de0 --- /dev/null +++ b/scripts/POSIX/mizf @@ -0,0 +1,42 @@ +#!/bin/sh +# +# Mizar Verifier, example shell command +# + +accommodate() +{ + makeenv $1 + if [ "$?" = "0" ] + then + verify $1 + else + errflag $1 + addfmsg $1 $MIZFILES/mizar + exit 2 + fi +} + +verify() +{ + verifier $1 + errflag $1 + addfmsg $1 $MIZFILES/mizar +} + +if [ -z "$1" ] + then + echo "> `basename $0` error : Missing parameter" + echo "Usage: `basename $0` mizar_article_name" + if [ -n "$MIZFILES" ] + then + MizarReleaseNbr=`awk -F= '/MizarReleaseNbr/{print $2}' $MIZFILES/mml.ini` + MizarVersionNbr=`awk -F= '/MizarVersionNbr/{print $2}' $MIZFILES/mml.ini` + MizarVariantNbr=`awk -F= '/MizarVariantNbr/{print $2}' $MIZFILES/mml.ini` + MMLVersion=`awk -F= '/MMLVersion/{print $2}' $MIZFILES/mml.ini` + NumberOfArticles=`awk -F= '/NumberOfArticles/{print $2}' $MIZFILES/mml.ini` + echo "MML ver. $MMLVersion.$NumberOfArticles for Mizar ver. $MizarReleaseNbr.$MizarVersionNbr.$MizarVariantNbr available in $MIZFILES" + fi + exit 1 + else + accommodate "`dirname $1`/`basename $1 .miz`" +fi diff --git a/scripts/POSIX/revedt b/scripts/POSIX/revedt new file mode 100755 index 0000000..f4fa8eb --- /dev/null +++ b/scripts/POSIX/revedt @@ -0,0 +1,34 @@ +#!/bin/sh +# +# Mizar editing utilities, example shell command +# + +accommodate() +{ + makeenv $1 + if test "$?" = "0" + then + verify $1 + else + errflag $1 + addfmsg $1 $MIZFILES/mizar + exit 2 + fi +} + +verify() +{ + $VERIFIER $1 + edtfile $1 + cp $1.'$-$' $1.miz +} + +if test -z "$1" -o -z "$2" + then + echo "> `basename $0` error : Missing parameter" + echo "Usage: `basename $0` mizar_utility_name mizar_article_name" + exit 1 + else + VERIFIER=$1 + accommodate "`dirname $2`/`basename $2 .miz`" +fi diff --git a/scripts/POSIX/revf b/scripts/POSIX/revf new file mode 100755 index 0000000..0c03896 --- /dev/null +++ b/scripts/POSIX/revf @@ -0,0 +1,34 @@ +#!/bin/sh +# +# Mizar utilities, example shell command +# + +accommodate() +{ + makeenv $1 + if test "$?" = "0" + then + verify $1 + else + errflag $1 + addfmsg $1 $MIZFILES/mizar + exit 2 + fi +} + +verify() +{ + $VERIFIER $1 + errflag $1 + addfmsg $1 $MIZFILES/mizar +} + +if test -z "$1" -o -z "$2" + then + echo "> `basename $0` error : Missing parameter" + echo "Usage: `basename $0` mizar_utility_name mizar_article_name" + exit 1 + else + VERIFIER=$1 + accommodate "`dirname $2`/`basename $2 .miz`" +fi diff --git a/scripts/WINDOWS/clrenv.bat b/scripts/WINDOWS/clrenv.bat new file mode 100644 index 0000000..07ea531 --- /dev/null +++ b/scripts/WINDOWS/clrenv.bat @@ -0,0 +1,73 @@ +@echo off +:; +:; The batch file for cleaning environment declaration. +:; Enter the filename without an extension. The article +:; should report no errors. The list of removed identifiers +:; is in the file clearenv.log. +:; +if "%1"=="" goto end +set MIZ_YES= +%MIZFILES%\accom text\%1 +%MIZFILES%\chkerr text\%1 +if ErrorLevel 1 goto finish +%MIZFILES%\verifier -qs text\%1 +%MIZFILES%\chkerr text\%1 +if ErrorLevel 1 goto finish +call :clrw32 %1 notations +call :clrw32 %1 definitions +call :clrw32 %1 expansions +call :clrw32 %1 equalities +call :clrw32 %1 requirements +call :clrw32 %1 registrations +call :clrw32 %1 constructors +%MIZFILES%\remflags text\%1.miz +goto bye +:end +echo. +echo Enter article name as a parameter. +echo. +goto bye +:finish +echo. +echo Your article reports errors. Remove them and try once more. +echo. +goto bye +:clrw32 +%MIZFILES%\msplit text\%1 +%MIZFILES%\commextr text\%1 +echo 0 >text\%1.cospr.txt +echo %2>>text\%1.cospr.txt +echo. >>text\%1.cospr.txt +%MIZFILES%\clearenv text\%1 ZERO +set /P MIZ_NBR= nul +if exist %1.dcl del %1.dcl >nul +if exist %1.dco del %1.dco >nul +if exist %1.def del %1.def >nul +if exist %1.the del %1.the >nul +if exist %1.sch del %1.sch >nul +echo Local data base created. +:end + diff --git a/scripts/WINDOWS/mizf.bat b/scripts/WINDOWS/mizf.bat new file mode 100644 index 0000000..a2f5992 --- /dev/null +++ b/scripts/WINDOWS/mizf.bat @@ -0,0 +1,34 @@ +@echo off +rem +rem PC Mizar Verifier, BATCH command +rem +if "%1"=="" goto exit +for %%F in (A,a) do if "%1"=="/%%F-" shift +if "%mizfiles%"=="" set mizfiles=c:\mizar +if exist %mizfiles%\verifier.exe goto mizfiles +echo Can't find %mizfiles%\verifier.exe +goto exit +:mizfiles +for %%F in (A,a) do if "%1"=="/%%F+" goto s_accom +for %%F in (A,a) do if "%2"=="/%%F+" goto accom +%mizfiles%\makeenv %1 +%mizfiles%\chkerr %1 +if not ErrorLevel 1 goto continue +%mizfiles%\errflag %1 +%mizfiles%\addfmsg %1 %mizfiles%\mizar +goto exit +:s_accom +shift +:accom +%mizfiles%\accom %1 +%mizfiles%\chkerr %1 +if not ErrorLevel 1 goto continue +%mizfiles%\errflag %1 +%mizfiles%\addfmsg %1 %mizfiles%\mizar +goto exit +:continue +%mizfiles%\verifier %1 +%mizfiles%\errflag %1 +%mizfiles%\addfmsg %1 %mizfiles%\mizar +:exit +if exist *.$$$ del *.$$$ diff --git a/scripts/WINDOWS/mizgrep.bat b/scripts/WINDOWS/mizgrep.bat new file mode 100644 index 0000000..d9f60e2 --- /dev/null +++ b/scripts/WINDOWS/mizgrep.bat @@ -0,0 +1,2 @@ +@echo off +FOR /F "tokens=1 delims=" %%A in ('type %MIZFILES%\mml.lar') do grep -H %1 %2 %3 %MIZFILES%\%4\%%A.%5 diff --git a/scripts/WINDOWS/revedt.bat b/scripts/WINDOWS/revedt.bat new file mode 100644 index 0000000..283551a --- /dev/null +++ b/scripts/WINDOWS/revedt.bat @@ -0,0 +1,37 @@ +@echo off +rem +rem Mizar revision utility batch +rem +if "%1"=="" goto usage +for %%F in (A,a) do if "%1"=="/%%F-" shift +if "%mizfiles%"=="" set mizfiles=c:\mizar +:mizfiles +for %%F in (A,a) do if "%1"=="/%%F+" goto s_accom +for %%F in (A,a) do if "%3"=="/%%F+" goto accom +%mizfiles%\makeenv %2 +%mizfiles%\chkerr %2 +if not ErrorLevel 1 goto continue +%mizfiles%\errflag %2 +%mizfiles%\addfmsg %2 %mizfiles%\mizar +goto exit +:s_accom +shift +:accom +%mizfiles%\accom %2 +%mizfiles%\chkerr %2 +if not ErrorLevel 1 goto continue +%mizfiles%\errflag %2 +%mizfiles%\addfmsg %2 %mizfiles%\mizar +goto exit +:continue +%1 %2 +%mizfiles%\edtfile %2 +copy %2.$-$ %2.miz +goto exit +:usage +echo ÿ +echo Mizar revision utility batch command +echo ÿ +echo Usage: revedt [ /a+ ] utility-name file-name +echo ÿ +:exit diff --git a/scripts/WINDOWS/revedt2.bat b/scripts/WINDOWS/revedt2.bat new file mode 100644 index 0000000..0c012a2 --- /dev/null +++ b/scripts/WINDOWS/revedt2.bat @@ -0,0 +1,39 @@ +@echo off +rem +rem Mizar revision utility batch for chkrprem +rem +if "%1"=="" goto usage +for %%F in (A,a) do if "%1"=="/%%F-" shift +if "%mizfiles%"=="" set mizfiles=c:\mizar +:mizfiles +for %%F in (A,a) do if "%1"=="/%%F+" goto s_accom +for %%F in (A,a) do if "%3"=="/%%F+" goto accom +%mizfiles%\makeenv %2 +%mizfiles%\chkerr %2 +if not ErrorLevel 1 goto continue +%mizfiles%\errflag %2 +%mizfiles%\addfmsg %2 %mizfiles%\mizar +goto exit +:s_accom +shift +:accom +%mizfiles%\accom %2 +%mizfiles%\chkerr %2 +if not ErrorLevel 1 goto continue +%mizfiles%\errflag %2 +%mizfiles%\addfmsg %2 %mizfiles%\mizar +goto exit +:continue +%1 %2 +copy %2.err %2.$er +%mizfiles%\refrem %2 +%mizfiles%\edtfile %2 +copy %2.$-$ %2.miz +goto exit +:usage +echo ÿ +echo Mizar revision utility batch command for chkrprem +echo ÿ +echo Usage: revedt2 [ /a+ ] utility-name file-name +echo ÿ +:exit diff --git a/scripts/WINDOWS/revf.bat b/scripts/WINDOWS/revf.bat new file mode 100644 index 0000000..ea45dfd --- /dev/null +++ b/scripts/WINDOWS/revf.bat @@ -0,0 +1,38 @@ +@echo off +rem +rem PC Mizar utilities BATCH command +rem +if "%1"=="" goto usage +for %%F in (A,a) do if "%1"=="/%%F-" shift +if "%mizfiles%"=="" set mizfiles=c:\mizar +:mizfiles +for %%F in (A,a) do if "%1"=="/%%F+" goto s_accom +for %%F in (A,a) do if "%3"=="/%%F+" goto accom +%mizfiles%\makeenv %2 +%mizfiles%\chkerr %2 +if not ErrorLevel 1 goto continue +%mizfiles%\errflag %2 +%mizfiles%\addfmsg %2 %mizfiles%\mizar +goto exit +:s_accom +shift +:accom +%mizfiles%\accom %2 +%mizfiles%\chkerr %2 +if not ErrorLevel 1 goto continue +%mizfiles%\errflag %2 +%mizfiles%\addfmsg %2 %mizfiles%\mizar +goto exit +:continue +%1 %2 +%mizfiles%\errflag %2 +%mizfiles%\addfmsg %2 %mizfiles%\mizar +goto exit +:usage +echo ÿ +echo PC Mizar utilities BATCH command +echo ÿ +echo Usage: revf [ /a+ ] utility-name file-name +echo ÿ +:exit +if exist *.$$$ del *.$$$