Merge pull request #1757 from herd/asl-code-snippets-bento

[ASL] removed code snippets information and bento tool

Author: Roman-Manevich

.github/workflows/build-asl-reference.yml

@@ -4,7 +4,6 @@ on:
   workflow_dispatch:
   pull_request:
     paths:
-      - 'internal/bento.mll'
       - 'asllib/doc/**'
       - 'asllib/aslspec/**'
       - '.github/workflows/build-asl-reference.yml'

Makefile

@@ -28,7 +28,6 @@ HERD_REGRESSION_TEST          = _build/default/internal/herd_regression_test.exe
 HERD_DIYCROSS_REGRESSION_TEST = _build/default/internal/herd_diycross_regression_test.exe
 HERD_CATALOGUE_REGRESSION_TEST = _build/default/internal/herd_catalogue_regression_test.exe
 HERD_ASSUMPTIONS_TEST		  = _build/default/internal/herd_assumptions_test.exe
-BENTO                         = _build/default/tools/bento.exe
 ASLREF                        = _build/default/asllib/aslref.exe
 CHECK_OBS                     = _build/default/internal/check_obs.exe
 all: build
@@ -975,8 +974,8 @@ clean-asl-pseudocode:
 
 .PHONY: asldoc
 asldoc: Version.ml
-	@ dune build -j $(J) --profile $(DUNE_PROFILE) $(BENTO) $(ASLREF)
-	@ $(MAKE) $(MFLAGS) -C asllib/doc all BENTO=$(CURDIR)/$(BENTO) ASLREF=$(CURDIR)/$(ASLREF)
+	@ dune build -j $(J) --profile $(DUNE_PROFILE) $(ASLREF)
+	@ $(MAKE) $(MFLAGS) -C asllib/doc all ASLREF=$(CURDIR)/$(ASLREF)
 
 .PHONY: clean-asldoc
 clean-asldoc:

asllib/doc/ASLReference.tex

@@ -5,15 +5,6 @@
 \input{ASLmacros}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% Macros for including code snippets from the ASLRef implementation
-\input{ASLTypingLines}
-\input{ASLSemanticsLines}
-\input{ASLTypeSatisfactionLines}
-\input{ASLStaticModelLines}
-\input{ASLStaticInterpreterLines}
-\input{ASLStaticEnvLines}
-\input{ASLASTUtilsLines}
-\input{ASLASTLines}
 \newcommand{\definitiontests}{../tests/ASLDefinition.t/}
 \newcommand{\syntaxtests}{../tests/ASLSyntaxReference.t/}
 \newcommand{\typingtests}{../tests/ASLTypingReference.t/}

asllib/doc/ASLmacros.tex

@@ -133,9 +133,6 @@
   % To visualize:
   % showframe
 ]{geometry}
-\input{ifempty}
-\input{ifcode}
-\input{control}
 
 \newcommand\aslrefterm[0]{\href{https://github.com/herd/herdtools7/tree/master/asllib}{aslref}}
 \newcommand\linuxbashshellterm[0]{Linux bash shell}
@@ -198,15 +195,6 @@
 \newcommand\ExampleDef[1]{\hypertarget{example-#1}{}\subsubsection{Example: #1}}
 \newcommand\ExampleRef[1]{\hyperlink{example-#1}{Example: #1}}
 
-\ifcode
-% First argument is \<rule>Begin, second is \<rule>End, third is the file name.
-% Example: for SemanticsRule.Lit, use the following:
-% \CodeSubsection{\LitBegin}{\LitEnd}{../Interpreter.ml}
-\newcommand\CodeSubsection[3]{\subsection{Code} \VerbatimInput[firstline=#1, lastline=#2]{#3}}
-\else
-\newcommand\CodeSubsection[3]{}
-\fi
-
 \definecolor{verylightgray}{rgb}{240,240,240}
 
 \newcommand\ASLListing[3]{
@@ -215,14 +203,10 @@
 \end{center}
 }
 
-\ifcode
 % First argument is \<rule>Begin, second is \<rule>End, third is the file name.
 % Example: for SemanticsRule.Lit, use the following:
 % \CodeSubsubsection{\LitBegin}{\LitEnd}{../Interpreter.ml}
-\newcommand\CodeSubsubsection[3]{\subsubsection{Code} \VerbatimInput[firstline=#1, lastline=#2]{#3}}
-\else
-\newcommand\CodeSubsubsection[3]{}
-\fi
+\newcommand\CodeSubsection[3]{}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Typesetting macros

asllib/doc/Makefile

@@ -1,4 +1,3 @@
-BENTO=../../_build/default/tools/bento.exe
 ASLREF=../../_build/install/default/bin/aslref
 LATEX=pdflatex
 BIBTEX=bibtex
@@ -9,27 +8,9 @@ GENERATED_ELEMENTS_TEX=generated_elements.tex
 
 all: generated_spec $(PDFS)
 
-short:
-	$(MAKE) $(MFLAGS) NOEMPTY=1 all
-
-code:
-	$(MAKE) $(MFLAGS) CODE=1 all
-
-no-empty:
-	$(MAKE) $(MFLAGS) NOEMPTY=1 all
-
-CONTROLS=ifempty.tex ifcode.tex
-
-.PHONY: control
-control: control.tex $(CONTROLS)
-
 LATEXMK=latexmk
 
-ASLReference.pdf: control\
-				ASLASTLines.tex ASLTypeSatisfactionLines.tex ASLStaticModelLines.tex ASLStaticInterpreterLines.tex\
-				ASLStaticEnvLines.tex ASLEnvLines.tex ASLASTUtilsLines.tex\
-				ASLTypingLines.tex ASLSemanticsLines.tex ASLStaticOperationsLines.tex\
-				desugarLines.tex
+ASLReference.pdf:
 	if command -v $(LATEXMK) >/dev/null 2>&1; \
 	then \
 		$(LATEXMK) -pdf ASLReference.tex; \
@@ -45,46 +26,9 @@ ASLReference.pdf: control\
 generated_spec: asl.spec
 	dune exec -- aslspec --render asl.spec;
 
-ASLASTLines.tex: ../AST.mli
-	$(BENTO) $< > $@
-
-ASLTypeSatisfactionLines.tex: ../types.ml
-	$(BENTO) $< > $@
-
-ASLEnvLines.tex: ../env.ml
-	$(BENTO) $< > $@
-
-ASLSemanticsLines.tex: ../Interpreter.ml
-	$(BENTO) $< > $@
-
-desugarLines.tex: ../desugar.ml
-	$(BENTO) $< > $@
-
-ASL%Lines.tex: ../%.ml
-	$(BENTO) $< > $@
-
-.PHONY: force
-
-ifdef CODE
-ifcode.tex: force
-	@echo "\\\\newif\\ifcode\\\\codetrue" >$@
-else
-ifcode.tex: force
-	@echo "\\\\newif\\ifcode\\\\codefalse" >$@
-endif
-
-ifdef SHOW_EMPTY
-ifempty.tex: force
-	@echo "\\\\newif\\ifempty\\\\emptytrue" >$@
-else
-ifempty.tex: force
-	@echo "\\\\newif\\ifempty\\\\emptyfalse" >$@
-endif
-
 .PHONY: clean
 clean:
 	/bin/rm -f $(PDFS)
-	/bin/rm -f *Lines.tex
 	/bin/rm -f $(GENERATED_ELEMENTS_TEX)
 	/bin/rm -f *.aux *.log *.fls *.log *.toc *.fdb_latexmk *~
 	/bin/rm -f $(CONTROLS)

asllib/doc/Statements.tex

@@ -2044,7 +2044,7 @@ \subsection{Semantics}
 
 
 \RenderProseAndFormally{eval_stmt_SReturn}
-\CodeSubsubsection{\SReturnBegin}{\EvalSReturnEnd}{../Interpreter.ml}
+\CodeSubsection{\SReturnBegin}{\EvalSReturnEnd}{../Interpreter.ml}
 
 \SemanticsRuleDef{EExprListM}
 \RenderRelation{eval_expr_list_m}

asllib/doc/control.tex

@@ -10,7 +10,6 @@
  mheader
  splitdot
  trTrue
- bento
  lexMiaou)
 
 (executables
@@ -52,7 +51,6 @@
   cat2html
   mlog2name
   mcat2includes
-  bento
   miaou
   cat2lisp
   dot2desc
@@ -95,7 +93,6 @@
   cat2html7
   mlog2name7
   mcat2includes7
-  bento
   miaou7
   cat2lisp
   dot2desc7