HomeIsabelle/Phabricator

Mark inline shim functions generated by the optimiser differently from those…

Description

Mark inline shim functions generated by the optimiser differently from those marked as inlineable because they
are small. The change at 8e4d341 meant that when maxInlineSize was very small the shim functions were not being
inlined resulting in the optimiser/simplifier getting into a loop. e.g. Tests/Succeed/Test140.ML.

Details

Provenance
dcjmAuthored on Aug 8 2020, 9:46 AM
Parents
rPOLYMLd57a84907afa: Poll should still pause if there are no descriptors. Fix problem with OS.
Branches
Unknown
Tags
Unknown