Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
# Ignore intermediate binary files generated by the compiler process
obj/*.o
obj/*.ppu
76 changes: 76 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
@@ -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)/
4 changes: 4 additions & 0 deletions bin/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
# Ignore everything in this directory
*
# ...except for this file
!.gitignore
4 changes: 4 additions & 0 deletions obj/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
# Ignore everything in this directory
*
# ...except for this file
!.gitignore
34 changes: 34 additions & 0 deletions scripts/POSIX/miz2abs
Original file line number Diff line number Diff line change
@@ -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

52 changes: 52 additions & 0 deletions scripts/POSIX/miz2prel
Original file line number Diff line number Diff line change
@@ -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
42 changes: 42 additions & 0 deletions scripts/POSIX/mizf
Original file line number Diff line number Diff line change
@@ -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
34 changes: 34 additions & 0 deletions scripts/POSIX/revedt
Original file line number Diff line number Diff line change
@@ -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
34 changes: 34 additions & 0 deletions scripts/POSIX/revf
Original file line number Diff line number Diff line change
@@ -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
73 changes: 73 additions & 0 deletions scripts/WINDOWS/clrenv.bat
Original file line number Diff line number Diff line change
@@ -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= <text\%1.cospr.txt
if %MIZ_NBR%==0 goto end
:loop
%MIZFILES%\clearenv text\%1 PREP %MIZ_NBR%
%MIZFILES%\createvd text\%1
%MIZFILES%\mglue text\%1
%MIZFILES%\accom text\%1
%MIZFILES%\errflag text\%1
%MIZFILES%\chkerr text\%1
if ErrorLevel 1 goto bad
%MIZFILES%\verifier -sq text\%1
%MIZFILES%\errflag text\%1
%MIZFILES%\chkerr text\%1
if ErrorLevel 1 goto bad
set MIZ_YES=NIE
%MIZFILES%\clearenv text\%1 %MIZ_YES% %MIZ_NBR%
goto good
:bad
set MIZ_YES=TAK
%MIZFILES%\clearenv text\%1 %MIZ_YES% %MIZ_NBR%
goto last
:good
:last
%MIZFILES%\createvd text\%1
%MIZFILES%\mglue text\%1
%MIZFILES%\accom text\%1
set /A MIZ_NBR-=1
if not %MIZ_NBR%==0 goto loop
:end
set MIZ_NBR=
:bye

21 changes: 21 additions & 0 deletions scripts/WINDOWS/miz2abs.bat
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
@echo off
rem
rem PC Mizar abstractor BATCH command
rem
if "%1"=="" goto exit
if "%mizfiles%"=="" set mizfiles=c:\mizar
if exist %mizfiles%\absedt.exe goto mizfiles
echo Can't find %mizfiles%\absedt.exe
goto exit
:mizfiles
%mizfiles%\accom %1
%mizfiles%\chkerr %1
if not ErrorLevel 1 goto continue
echo There are some accomodator errors
goto exit
:continue
%mizfiles%\absedt %1
%mizfiles%\edtfile %1
copy %1.$-$ %1.abs
echo Abstract file %1.abs created.
:exit
Loading