Skip to content

Commit

Permalink
Revert "Makefile: only use dune --release on release builds"
Browse files Browse the repository at this point in the history
For whatever reason, building the library without the --release flag
makes a dune build call in everparse for the ASN1 parser explode with a
stack overflow:
```
$ dune clean && fstar.exe --ocamlenv dune build
File "dune", lines 3-9, characters 0-113:
3 | (executable
4 |   (name ASN1_Parser)
5 |   (libraries
6 |     fstar.lib
7 |   )
8 |   (flags (:standard -w -8-9-11-26-27-33-39-20))
9 | )
Fatal error: exception Stack overflow
```
This is during compilation of the ASN1_X509.ml module, which is
58k lines long, and the offending function where the crash happens
(dparse_cert) is 28k lines long.

This is probably hitting some limitation of ocamlopt, but also a
reminder that we should try to generate more compact code. For now, just
revert this, and pay some time in development builds.

This reverts commit 1ac7ed0.
  • Loading branch information
mtzguido committed Feb 18, 2025
1 parent 380aea3 commit 4fee358
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 8 deletions.
14 changes: 7 additions & 7 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ $(FSTAR1_FULL_EXE): .bare1.src.touch .full1.src.touch .stage1.ml.touch $(MAYBEFO

$(FSTAR2_BARE_EXE): .bare2.src.touch .stage2.ml.touch $(MAYBEFORCE)
$(call bold_msg, "BUILD", "STAGE 2 FSTARC-BARE")
$(MAKE) -C stage2 fstarc-bare
$(MAKE) -C stage2 fstarc-bare FSTAR_DUNE_RELEASE=1
touch -c $@
# ^ Note, even if we don't release fstar-bare itself,
# it is still part of the build of the full fstar, so
Expand All @@ -191,7 +191,7 @@ $(FSTAR2_BARE_EXE): .bare2.src.touch .stage2.ml.touch $(MAYBEFORCE)

$(FSTAR2_FULL_EXE): .bare2.src.touch .full2.src.touch .stage2.ml.touch $(MAYBEFORCE)
$(call bold_msg, "BUILD", "STAGE 2 FSTARC")
$(MAKE) -C stage2 fstarc-full
$(MAKE) -C stage2 fstarc-full FSTAR_DUNE_RELEASE=1
touch -c $@

.alib2.src.touch: $(FSTAR2_FULL_EXE) .force
Expand All @@ -209,7 +209,7 @@ $(FSTAR2_FULL_EXE): .bare2.src.touch .full2.src.touch .stage2.ml.touch $(MAYBEFO

.alib2.touch: .alib2.src.touch .stage2.ml.touch $(MAYBEFORCE)
$(call bold_msg, "BUILD", "STAGE 2 LIB")
$(MAKE) -C stage2/ libapp
$(MAKE) -C stage2/ libapp FSTAR_DUNE_RELEASE=1
touch $@

.plib2.src.touch: $(FSTAR2_FULL_EXE) .alib2.src.touch .force
Expand All @@ -229,7 +229,7 @@ $(FSTAR2_FULL_EXE): .bare2.src.touch .full2.src.touch .stage2.ml.touch $(MAYBEFO

.plib2.touch: .plib2.src.touch .stage2.ml.touch $(MAYBEFORCE)
$(call bold_msg, "BUILD", "STAGE 2 PLUGLIB")
$(MAKE) -C stage2/ libplugin
$(MAKE) -C stage2/ libplugin FSTAR_DUNE_RELEASE=1
touch $@

# F# library, from stage 2.
Expand Down Expand Up @@ -298,7 +298,7 @@ endif
.install-stage2.touch: export FSTAR_LINK_LIBDIRS=$(LINK_OK)
.install-stage2.touch: .stage2.src.touch
$(call bold_msg, "INSTALL", "STAGE 2")
$(MAKE) -C stage2 install PREFIX=$(CURDIR)/stage2/out
$(MAKE) -C stage2 install PREFIX=$(CURDIR)/stage2/out FSTAR_DUNE_RELEASE=1
@# ^ pass PREFIX to make sure we don't get it from env
touch $@

Expand Down Expand Up @@ -326,14 +326,14 @@ install: export PREFIX?=/usr/local
install: export FSTAR_LINK_LIBDIRS=0 # default is false, but set anyway
install:
$(call bold_msg, "INSTALL", "STAGE 2")
$(MAKE) -C stage2 install
$(MAKE) -C stage2 install FSTAR_DUNE_RELEASE=1

__do-install-stage1:
$(call bold_msg, "INSTALL", "STAGE 1")
$(MAKE) -C stage1 install
__do-install-stage2:
$(call bold_msg, "INSTALL", "STAGE 2")
$(MAKE) -C stage2 install
$(MAKE) -C stage2 install FSTAR_DUNE_RELEASE=1

__do-archive: .force
rm -rf $(PKGTMP)
Expand Down
2 changes: 1 addition & 1 deletion mk/stage.mk
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ FSTAR_DUNE_OPTIONS += --display=quiet
endif

FSTAR_DUNE_BUILD_OPTIONS := $(FSTAR_DUNE_OPTIONS)
ifeq ($(FSTAR_RELEASE),1)
ifeq ($(FSTAR_DUNE_RELEASE),1)
FSTAR_DUNE_BUILD_OPTIONS += --release
endif

Expand Down

0 comments on commit 4fee358

Please sign in to comment.